# Applying Chevalley's Theorem to Elimination of quantifiers

In Vakil's FOAG, p218, he states Chevalley's theorem as follows

7.4.2 Chevally's Theroem---If $$\pi:X \to Y$$ is a finite type morphism of Noetherian schemes, the image of any constructible set is constructible. In particular, the image of $$\pi$$ is constructible.

And the following is 7.4.P.Exercise at page 221, in which Chevally's theorem is used.

In my understanding, the scheme $$X$$ is a open subscheme $$D(g_1,...,g_q)$$ of the closed subscheme $$\mathrm{Spec}(k[W_1,...,W_m,...X_1,..,X_n]/(f_1,...,f_p))$$ of $$\mathbb{A}^{n+m}$$. Is that right? But then I can't figure out why $$\pi$$ in the commutative diagram is a morphism of finite type, which is necessary to use Chevalley's theorem. Could you help me? Thanks in advance.

The inclusion $$X \hookrightarrow \mathbb{A}^{m+n}$$ is of finite type. Observe that we may factor this inclusion by $$D(g_1,\ldots,g_q) \hookrightarrow V(f_1,\ldots,f_p) \hookrightarrow \operatorname{Spec}k[W_1,\ldots,W_m,X_1,\ldots,X_n]$$. First, the inclusion $$V(f_1,\ldots,f_p) \hookrightarrow \operatorname{Spec}k[W_1,\ldots,W_m,X_1,\ldots,X_n]$$ is of finite-type as $$A :=k[W_1,\ldots,W_m,X_1,\ldots,X_n]/(f_1,\ldots,f_p)$$ is a finitely generated $$k[W_1,\ldots,W_m,X_1,\ldots,X_n]$$-algebra. Second, each $$D(g_i)$$ is affine and its coordinate ring is $$A_{g_i}$$ which is of finite-type over $$A$$. This yields that the inclusion $$D(g_1,\ldots,g_q) \hookrightarrow V(f_1,\ldots,f_p)$$ is locally of finite-type. The fact that there are finite $$g_i$$'s yields finite-type. Composition of finite-type morphisms is finite-type. Then $$X \hookrightarrow \mathbb{A}^{m+n}$$ is of finite-type. Finally the projection $$\mathbb{A}^{m+n} \to \mathbb{A}^n$$ is trivially of finite-type.
The argument actually concludes that every locally closed immersion $$Z \hookrightarrow Y$$ is locally of finite-type.