Properness survives composition

By [F1] and [F2], both $f$ and $g$ are locally of finite type. For any $x\in X$, refine affine neighbourhoods around $x$, $f(x)$, and $g(f(x))$ so that their coordinate-ring maps are finite type, using [F3]. If the two maps are $A\to B$ and $B\to C$, finite generating lists for $B\mathrm{/}A$ and $C\mathrm{/}B$ give a finite generating list for $C\mathrm{/}A$ by [F4]. Thus $g\circ f$ is locally of finite type.

Let $W\subseteq S$ be any quasi-compact open. Then $g^{-1}(W)$ is quasi-compact by [F5]. Its affine open cover from [F7] has a finite subcover $V_1,\dots ,V_n$; each $V_i$ is quasi-compact by [F6], so $f^{-1}(V_i)$ is quasi-compact by [F5]. Their finite union is $(g\circ f{)}^{-1}(W)$, which is therefore quasi-compact. Since $W$ was arbitrary, $g\circ f$ is quasi-compact, and [F2] makes it of finite type. If $g^{-1}(W)$ is empty, the finite subcover is empty and the same conclusion holds.

Let $i:Z\to Y$ and $j:Y\to T$ be closed immersions. Their composite is a homeomorphism onto a closed subset: $j(Y)$ is closed in $T$, and $j(i(Z))$ is closed in the subspace $j(Y)$. By [F13], $j_{\ast }{i}_{\ast }{\mathcal{O}}_Z$ equals $(j\circ i{)}_{\ast }{\mathcal{O}}_Z$. For any sheaf $\mathcal{G}$ on $Y$, [F13]--[F14] show that $(j_{\ast }\mathcal{G}{)}_t$ is ${\mathcal{G}}_y$ at $t=j(y)$ and is zero outside $j(Y)$: at an image point, open neighbourhoods restrict to a neighbourhood basis in $Y$; outside the closed image, some neighbourhood has empty inverse image. The map $j_{\ast }{\mathcal{O}}_Y\to j_{\ast }{i}_{\ast }{\mathcal{O}}_Z$ is therefore surjective on every stalk, since the stalk map ${\mathcal{O}}_{Y,y}\to (i_{\ast }{\mathcal{O}}_Z{)}_y$ is surjective by [F12]. By [F15] it is a surjection of sheaves; composing with the surjection ${\mathcal{O}}_T\to j_{\ast }{\mathcal{O}}_Y$ proves that ${\mathcal{O}}_T\to (j\circ i{)}_{\ast }{\mathcal{O}}_Z$ is surjective. Thus the composite is a closed immersion by [F12].

Let $T\to S$ be arbitrary and put $Y_T=Y{\times }_{S}T$. The maps $Y_T\to T$ and $X{\times }_Y{Y}_T\to Y_T$ are base changes of $g$ and $f$, respectively; they are closed because both original maps are universally closed by [F1] and [F19]. By [F17]--[F18], $X{\times }_Y(Y{\times }_{S}T)\cong X{\times }_{S}T$ compatibly with the maps to $T$. Thus the base change of $g\circ f$ to $T$ is the composite of these two closed maps, hence is closed. Since $T$ was arbitrary, [F19] makes $g\circ f$ universally closed.

By [F1] and [F8], both diagonals ${\mathrm{\Delta }}_{X\mathrm{/}Y}$ and ${\mathrm{\Delta }}_{Y\mathrm{/}S}$ are closed immersions. The map $u:X{\times }_{Y}X\to X{\times }_{S}X$ is the pullback of ${\mathrm{\Delta }}_{Y\mathrm{/}S}$ along $f{\times }_{S}f$: a test pair $(a,b)$ into $X{\times }_{S}X$ factors through that pullback exactly when $f\circ a$ equals $f\circ b$. Hence $u$ is a closed immersion by [F10]--[F11]. The composite $u\circ {\mathrm{\Delta }}_{X\mathrm{/}Y}$ has identity composites with both projections, so equals ${\mathrm{\Delta }}_{X\mathrm{/}S}$ by [F9]. Step 1.3 makes this diagonal a closed immersion, and [F8] makes $g\circ f$ separated.

Steps 1.1--1.2, 2.1, and 1.4 prove that $g\circ f$ is of finite type, separated, and universally closed, so it is proper by [F1]. If $X$ is empty, the composite is empty and these conditions hold; if $Y$ is empty then $X$ is empty. Empty and zero-ring affine charts cause no exception, and the identity morphism is covered by empty generator lists and singleton affine covers. The statement has no endpoint or iff cases. AC is used only in step 2.1 as declared above; the finite chart and generator arguments are pointwise or finite and do not use arbitrary-index choice.