The smooth locus is open

Fix $x\in \mathrm{Sm}(f)$, write $\mathfrak{q}$ for the prime of $C$ corresponding to $x$ in an affine chart, and put $s=f(x)$. By [F2] there are affine opens $U=\mathrm{Spec}C$ of $x$ and $V=\mathrm{Spec}A$ of $s$ with $f(U)\subseteq V$ and, for some $h\in C\setminus \mathfrak{q}$, a presentation $C_h\cong (A[t_1,\dots ,t_m]\mathrm{/}(f_1,\dots ,f_r){)}_g$ in which an $r\times r$ Jacobian minor has image a unit of $C_h$.

Let $x^{\mathrm{\prime }}\in D(h)\subseteq U$ and let ${\mathfrak{q}}^{\mathrm{\prime }}\in \mathrm{Spec}C$ be the corresponding prime; then $h\mathrm{\notin }{\mathfrak{q}}^{\mathrm{\prime }}$. The same neighbourhoods $U$ and $V$ and the same element $h$ with the same presentation satisfy the criterion of [F2] at $x^{\mathrm{\prime }}$, since the displayed presentation of $C_h$ has its Jacobian minor invertible in $C_h$ and $h\in C\setminus {\mathfrak{q}}^{\mathrm{\prime }}$; hence $f$ is smooth at $x^{\mathrm{\prime }}$. As $x^{\mathrm{\prime }}\in D(h)$ was arbitrary, $D(h)\subseteq \mathrm{Sm}(f)$.

The set $D(h)$ is open in $U$ by [F4] and contains $x$ by [F2]. Thus every point $x\in \mathrm{Sm}(f)$ has an open neighbourhood $D(h)\subseteq X$ contained in $\mathrm{Sm}(f)$, so $\mathrm{Sm}(f)$ is open in $X$.

The restriction $f{\mathrm{\mid }}_{\mathrm{Sm}(f)}$ is smooth: at each $x\in \mathrm{Sm}(f)$ the morphism $f$ is smooth at $x$ by the definition of the locus, and smoothness at a point is preserved by restricting the source to an open neighbourhood of that point, so the restriction is smooth at every point of $\mathrm{Sm}(f)$, hence smooth.

If $X=\mathrm{\varnothing }$ then $\mathrm{Sm}(f)=\mathrm{\varnothing }$ is open and the empty restriction is smooth by [F1]; otherwise the argument of steps 1.1, 2.1, 3.1 and 4.1 applies at every point of the locus. The Axiom of Choice [F5] is assumed in the Statement and used exactly through the criterion [F2], invoked in steps 1.1 and 2.1. [F1, F2, F5, step 4.1] $\mathrm{\square }$