A proper quasi-finite morphism is finite

Finiteness is local on the base by [F5], so replace $S$ by an affine open in a cover on which [F1] supplies $f=g\circ j$ with $j:X\hookrightarrow \bar{X}$ open and $g:\bar{X}\to S$ finite. Since $f$ is proper it is separated, as required by [F1]. By [F2] the finite morphism $g$ is separated, so [F3] applied to the $S$-map $j$ makes $j$ proper.

The image $j(X)$ is open in $\bar{X}$ because $j$ is an open immersion, and closed because $j$ is proper and hence a closed map by [F3]. Thus it is open and closed. An open immersion identifies $X$ with the open subscheme $j(X)$; because its complement is also open, the same inclusion is a closed immersion. On any affine open $\mathrm{Spec}B$ of $\bar{X}$, [F4] therefore writes the corresponding part of $X$ as $\mathrm{Spec}(B\mathrm{/}I)$.

For an affine open $\mathrm{Spec}A\subseteq S$, finiteness of $g$ gives $g^{-1}(\mathrm{Spec}A)=\mathrm{Spec}B$ with $B$ finite as an $A$-module. By step 2.1 the inverse image under $f$ is $\mathrm{Spec}(B\mathrm{/}I)$ for an ideal $I$, and $B\mathrm{/}I$ is a quotient of the finite $A$-module $B$. Hence $f$ is finite over this affine base by [F5]. The base-local conclusions glue to give finiteness over all of $S$.

If $X=\mathrm{\varnothing }$, the coordinate algebra is the zero ring, finite as an $A$-module, and the argument still applies. No reducedness or Noetherian hypothesis is used. AC enters only through the invoked suppliers in [F1] and [F4]; the scheme-level factorization is supplied by [F1].