Properness descends from a surjective source (source code)

= Properness descends from a surjective source

Suppose $gf$ is proper, $f$ is surjective, and $g$ is separated and of finite type. Surjectivity of scheme morphisms is preserved by base change: a nonempty fiber remains nonempty after a residue-field extension. After any base change to $Z$, for a closed subset $C$ of the new target of $f$, its inverse image is closed and has image $g(C)$ under the proper composite. Thus $g(C)$ is closed. This proves universal closedness of $g$, completing the three conditions for properness.