Finite morphisms are proper

By [F2] the morphism $f$ is affine: for every affine open $U=\mathrm{Spec}A\subseteq S$ the inverse image $f^{-1}(U)$ is affine. This implication uses only the definition of finiteness and no choice.

The morphism $f$ is locally of finite type. Let $x\in X$. By [F8] the point $f(x)$ has an affine open neighbourhood $V=\mathrm{Spec}A\subseteq S$; then $U:=f^{-1}(V)$ is affine, say $U=\mathrm{Spec}B$, and contains $x$, and $B$ is module-finite over $A$ by [F1]. Hence $B$ is of finite type over $A$ by [F4], and $f(U)\subseteq V$; so $x$ has a finite-type affine chart over an affine open of $S$, and since $x$ was arbitrary, $f$ is locally of finite type by [F5].

The morphism $f$ is quasi-compact. For every affine open $V\subseteq S$ the inverse image $f^{-1}(V)$ is affine by [F1] and hence quasi-compact by [F6]; by the criterion [F7] this makes $f$ quasi-compact.

By [F3] the affine morphism $f$ is separated.

By [F5] the morphism $f$ is of finite type, being locally of finite type by step 1.2 and quasi-compact by step 1.3.

By [F9] the finite morphism $f$ is universally closed; this is the only step that uses the Axiom of Choice.

Steps 2.1, 2.2 and 2.3 give separatedness, finite typeness and universal closedness, so $f$ is proper by [F10]. The Axiom of Choice [F11] enters exactly through [F9], whose proof uses lying over for the integral maps $A\to B$; the finite-to-affine implication of [F2] used in step 1.1 is choice-free by its statement, and no further selection occurs. The empty morphism is included: if $X=\mathrm{\varnothing }$ then $f^{-1}(U)=\mathrm{\varnothing }=\mathrm{Spec}0$ over any affine $U$, and the zero ring is module-finite over $A$ by [F1], so $f$ is finite and the same argument applies; the finite-type chart condition of step 1.2 is vacuous in that case and the criterion of step 1.3 is satisfied by the empty scheme, which is affine and hence quasi-compact.