Solution (source code)

= Solution

We first justify <surjectivity is preserved by base change> for <morphisms of schemes>. Given $y'$ over $y$ and a point $x$ over $y$, the <fiber> after the residue-<field> extension contains a point because
$$
\kappa(x)\otimes_{\kappa(y)}\kappa(y')\ne0.
$$
Indeed, tensoring a nonzero <vector space> over a <field> with a <field extension> remains nonzero; a nonzero commutative <ring> has a <prime ideal>, giving the required point. Thus every <base change> of $f$ is surjective.

Now make an arbitrary <base change> $Z'\to Z$. For a closed subset $C\subseteq Y'=Y\times_ZZ'$, its inverse image under $f':X'\to Y'$ is closed. The <proper morphism> $(gf)':X'\to Z'$ therefore has closed image on that inverse image. Surjectivity of $f'$ gives
$$
g'(C)=(g'f')\bigl((f')^{-1}(C)\bigr),
$$
so $g'(C)$ is closed. This proves that $g$ is a <universally closed morphism>. Together with the given <separatedness> and <finite type>, it proves
$$
\boxed{gf\text{ proper},\ f\text{ surjective},\ g\text{ separated and of finite type}\ \Longrightarrow\ g\text{ proper}.}
$$