Projective morphisms are proper

By [F1] the morphism $f$ admits a factorization $f=\pi \circ i$ over $S$, where $n\ge 0$, $i:X\to {\mathbb{P}}_S^n$ is a closed immersion and $\pi :{\mathbb{P}}_S^n\to S$ is the projection of the relative projective space.

By the AC-qualified [F3] the closed immersion $i$ is finite, hence proper.

By the AC-qualified [F2] the projection $\pi :{\mathbb{P}}_S^n\to S$ is proper.

Since $f=\pi \circ i$ is a composite of the proper morphisms $i$ and $\pi$, the AC-qualified [F4] shows that $f$ is proper.

This proves the theorem for the finite-dimensional H-projective convention fixed in [F1]; the separate projective-bundle convention of the sources is not treated here and is not claimed. The Axiom of Choice [F5] is assumed and is used only through [F2], [F3] and [F4]. The degenerate cases are included: for $n=0$ the projection is the isomorphism ${\mathbb{P}}_S^0\cong S$ and $f$ is the closed immersion $i$; if $S=\mathrm{\varnothing }$ then ${\mathbb{P}}_S^n=X=\mathrm{\varnothing }$ and the morphisms are the empty ones; if $i$ is the identity then $f=\pi$ is the projection, proper by [F2]; and if $X=\mathrm{\varnothing }$ then $i$ is the empty closed immersion, proper by [F3]. No Noetherian, field, reducedness or nonemptiness hypothesis is imposed.