Projective space is of finite type over its base

Let $V=\mathrm{Spec}A\subseteq S$ be an affine open, which exists around every point of $S$ by [F8]. By [F1] the charts $U_0^A,\dots ,U_n^A$ are open subschemes forming an open cover of ${\pi }^{-1}(V)={\mathbb{P}}_A^n$, and $U_i^A=\mathrm{Spec}A[x_{\mathrm{\ell }}^{(i)}:\mathrm{\ell }\mathrm{\ne }i]$ is an affine scheme over $V$.

For each $i$ the ring map $A\to A[x_{\mathrm{\ell }}^{(i)}:\mathrm{\ell }\mathrm{\ne }i]$ is of finite type: when $n\ge 1$ the target polynomial algebra is generated as an $A$-algebra by its finitely many indeterminates, and when $n=0$ there is one chart with coordinate ring $A$, the identity map, which is of finite type by the empty generating list in [F2].

For every affine open $V=\mathrm{Spec}A\subseteq S$ the inverse image ${\pi }^{-1}(V)={\mathbb{P}}_A^n$ is the union of the finitely many affine charts $U_0^A,\dots ,U_n^A$, and each $U_i^A$ is quasi-compact by [F6]. A finite union of quasi-compact subspaces is quasi-compact: an open cover of the union restricts to an open cover of each $U_i^A$, from which finitely many members can be chosen by [F7], and the finitely many resulting subfamilies cover the union. Hence ${\pi }^{-1}(V)$ is quasi-compact.

By the affine-local criterion of [F3], steps 1.1 and 2.1 show that $\pi$ is locally of finite type: over each affine open $V=\mathrm{Spec}A\subseteq S$ the source is covered by the affine charts $U_i^A$ on which the ring map is of finite type.

By [F5] the morphism $\pi$ is quasi-compact, and by [F3] a quasi-compact morphism that is locally of finite type is of finite type; with step 3.1 this proves that $\pi :{\mathbb{P}}_S^n\to S$ is of finite type in the sense of [F4]. The empty base gives ${\mathbb{P}}_{\mathrm{\varnothing }}^n=\mathrm{\varnothing }$ and the empty morphism, which is of finite type vacuously, and for $n=0$ the unique chart has ${\mathbb{P}}_S^0\cong S$ with $\pi$ an isomorphism, included in the computations above.