The Stacks project

Proof. Lemma 98.13.8 applies to $F$. Using this we choose, for every finite type field $k$ over $S$ and $x_0 \in F(\mathop{\mathrm{Spec}}(k))$, an affine scheme $U_{k, x_0}$ of finite type over $S$ and a smooth morphism $U_{k, x_0} \to F$ such that there exists a finite type point $u_{k, x_0} \in U_{k, x_0}$ with residue field $k$ such that $x_0$ is the image of $u_{k, x_0}$. Then

is smooth¹. To finish the proof it suffices to show this map is surjective, see Bootstrap, Lemma 80.12.3 (this is where we use axiom [0]). By Criteria for Representability, Lemma 97.5.6 it suffices to show that $U \times _ F V \to V$ is surjective for those $V \to F$ where $V$ is an affine scheme locally of finite presentation over $S$. Since $U \times _ F V \to V$ is smooth the image is open. Hence it suffices to show that the image of $U \times _ F V \to V$ contains all finite type points of $V$, see Morphisms, Lemma 29.16.7. Let $v_0 \in V$ be a finite type point. Then $k = \kappa (v_0)$ is a finite type field over $S$. Denote $x_0$ the composition $\mathop{\mathrm{Spec}}(k) \xrightarrow {v_0} V \to F$. Then $(u_{k, x_0}, v_0) : \mathop{\mathrm{Spec}}(k) \to U \times _ F V$ is a point mapping to $v_0$ and we win. $\square$