Properness survives arbitrary base change

By [F1], $f$ is separated, of finite type, and universally closed; in particular, its diagonal ${\mathrm{\Delta }}_{X\mathrm{/}S}$ is a closed immersion by [F3].

By [F2], the base change $f_{S^{\mathrm{\prime }}}$ is of finite type.

By [F4], the diagonal ${\mathrm{\Delta }}_{X_{S^{\mathrm{\prime }}}\mathrm{/}{S}^{\mathrm{\prime }}}$ is the base change of ${\mathrm{\Delta }}_{X\mathrm{/}S}$. By the AC-qualified [F5] it is a closed immersion, so [F3] makes $f_{S^{\mathrm{\prime }}}$ separated. This is the only use of AC in the argument.

Let $T\to S^{\mathrm{\prime }}$ be any morphism. By [F7], the base change of $f_{S^{\mathrm{\prime }}}$ to $T$ is canonically isomorphic, compatibly with its projection to $T$, to the base change of $f$ along the composite $T\to S^{\mathrm{\prime }}\to S$. Since $f$ is universally closed by [F1], [F6] says this latter map is closed. Thus every base change of $f_{S^{\mathrm{\prime }}}$ is closed, and [F6] makes $f_{S^{\mathrm{\prime }}}$ universally closed.

The morphism $f_{S^{\mathrm{\prime }}}$ is separated by step 1.3, of finite type by step 1.2, and universally closed by step 1.4. Hence it is proper by [F1]. If $X$ is empty its pullback is empty; if $S$ is empty then $S^{\mathrm{\prime }}$ and $X$ are empty. Zero-ring affine charts remain empty under base change. For the identity $S^{\mathrm{\prime }}=S$, the assertion returns $f$. Nonreduced schemes and arbitrary bases are covered without additional hypotheses. There are no endpoint or equivalence cases.