Properness descends through fpqc base change

Put $X^{\mathrm{\prime }}=X{\times }_S{S}^{\mathrm{\prime }}$ and let $f^{\mathrm{\prime }}:X^{\mathrm{\prime }}\to S^{\mathrm{\prime }}$ be the second projection, so that $f^{\mathrm{\prime }}$ is the base change of $f$ along $p$ in the sense of [F5]. By [F2] the morphism $p$ is flat, surjective and quasi-compact, so it is an fpqc covering morphism in the page-local convention, and the hypotheses of [F3] and [F4] are satisfied by $p$, $f$ and $f^{\mathrm{\prime }}$. The fibre product exists for arbitrary schemes, so $f^{\mathrm{\prime }}$ is defined for every $f$ and every $p$.

Suppose first that $f$ is proper. The morphism $f^{\mathrm{\prime }}$ is a base change of $f$ along the arbitrary morphism $p$, so [F4] applies with hypothesis exactly the assumed properness of $f$, and $f^{\mathrm{\prime }}$ is proper. Unfolding [F1], this says that $f^{\mathrm{\prime }}$ is separated, of finite type and universally closed. This proves the forward implication.

Conversely, suppose that $f^{\mathrm{\prime }}$ is proper. By [F1], $f^{\mathrm{\prime }}$ is separated, of finite type and universally closed. Since $f^{\mathrm{\prime }}$ is the base change of $f$ along the fpqc covering morphism $p$ (step 1.1), [F3] applies to $p$ and $f$ and shows that $f$ likewise has each of these three properties: $f$ is separated, of finite type and universally closed. This proves the reverse implication.

By [F1], the three properties established in step 2.2 make $f$ proper. Together with step 2.1 this shows that $f$ is proper if and only if $f^{\mathrm{\prime }}$ is proper, which is the claim.

Degenerate cases and choice accounting. If $S$ is empty then $S^{\mathrm{\prime }}$ and $X$ are empty as well, and both $f$ and $f^{\mathrm{\prime }}$ are the empty morphism, which is separated, of finite type and universally closed vacuously, hence proper by [F1]; if $X$ is empty the same holds with $X^{\mathrm{\prime }}$ empty. If $p$ is the identity of $S$, then $f^{\mathrm{\prime }}=f$ and the equivalence is tautological. None of these cases requires an extra hypothesis, and nonreduced or non-Noetherian schemes are allowed throughout because [F1] imposes no such condition. AC is declared in the statement and is used exactly through [F3] and [F4]; no other step of the argument invokes it. Both directions of the biconditional were proved, the forward one in step 2.1 and the reverse one in step 2.2.