Lemma 2

Let $k$ be a field, and let $K$ and $L$ be extensions of $k$. Suppose that $K$ is of finite type and that one of the extensions $K$ or $L$ is separable. Then the ring $K \otimes_k L$ is regular.

Let $A$ denote the ring $K \otimes_k L$; it is noetherian by cor. of prop. 2 (No. 2). Suppose first that the extension $K$ is separable. By A, V, p. 130, corollary, there exists a transcendence basis $t = (t_1, \ldots, t_n)$ of $K$ such that $K$ is a finite separable extension of the pure extension $k(t)$. The ring $E = k(t) \otimes_k L$, isomorphic to a ring of fractions of a polynomial ring over $L$, is regular ($§ 4$, No. 2, cor. 5 of prop. 4); for every prime ideal $p$ of $E$, the ring $\kappa(p) \otimes_E A$ is isomorphic to $\kappa(p) \otimes_{k(t)} K$, hence to a finite product of fields (A, V, p. 35, def. 1, p. 34, th. 4, and p. 33, prop. 5). Since $A$ is a free $E$-module, it is a regular ring by cor. of prop. 9 of $§ 4$, No. 5.

Suppose now that $L$ is separable over $k$. By the first part of the proof, the ring $K \otimes_k L'$ is regular for every finite-type subextension $L'$ of $L$. One concludes by applying lemma 1.