A nonempty smooth scheme has a finite separable point

Extend scalars to $k_s$ from [F1]. Faithful scalar extension leaves $X_{k_s}$ nonempty. Smoothness is preserved: in local standard smooth presentations the invertible Jacobian minor stays invertible under scalar extension. By [F2], a nonempty affine open $U\subset X_{k_s}$ has an étale map to ${\mathbf{A}}_{k_s}^d$. Its image is a nonempty open set. The field $k_s$ is infinite: a finite separably closed field cannot exist, since $T^{q^2}-T$ would have separable roots outside a field of $q$ elements. A nonzero polynomial over an infinite field cannot vanish on all its affine-space points, by induction on the number of variables and the one-variable root bound. Hence every nonempty open in ${\mathbf{A}}_{k_s}^d$ contains a $k_s$-rational point. The nonempty étale fibre over such a point contains a point whose residue extension is finite separable by [F2], and is therefore $k_s$ itself. We have obtained a $k_s$-point of $X$.

In an affine finite-type chart $\mathrm{Spec}A\subset X$ containing its image, this point is a map $A\to k_s$. The image is generated by finitely many elements algebraic separable over $k$. They lie in a finite separable extension $L\mathrm{/}k$ by [F3]. The image $B\subset L$ is a finite-dimensional domain over $k$ and hence a field: multiplication by a nonzero element is an injective endomorphism of a finite-dimensional vector space and therefore surjective. Thus the kernel of $A\to k_s$ is maximal and its residue field $B$ is finite separable over $k$. The corresponding point is closed in $X$: if it specialized to another point, choose an affine neighbourhood of the specialization; it contains the original point, whose residue field is algebraic over $k$, so the same finite-type argument makes it maximal in that chart and forbids a strict specialization. AC is used through [F1] and [F2].