Affine geometric dimension equals ring dimension

The field $k$ has only the ideals 0 and $k$, hence is Noetherian. Iterating F2 makes R Noetherian. For every relatively closed subset $Z$ of X, polynomial defining equations show $V(I(Z))=Z$ in $k^n$. Thus a descending chain of closed subsets gives an ascending chain of vanishing ideals, whose stabilization forces stabilization of the closed sets. This makes X Noetherian and its geometric chain dimension well-defined.

If Z is nonempty irreducible closed, then $I(Z)$ is proper and prime: $fg$ vanishing on Z writes Z as the union of its closed zero loci for f and g, so one factor vanishes on all of Z. Conversely, if $I(Z)$ is prime and Z were the union of two proper closed subsets, choose a defining equation of each subset nonzero somewhere on Z. Their product vanishes on Z, contradicting primality. These choices are finite.

For every proper prime $P\supseteq I(X)$, F1 gives $I(V(P))=P$ since P is radical. In particular $V(P)$ is nonempty, since the empty set has vanishing ideal R; it lies in X and is irreducible by step 1.2. Together with $V(I(Z))=Z$, this gives inverse inclusion-reversing correspondences between nonempty irreducible closed subsets of X and primes of R containing I(X). This application of F1 is the precise inherited AC use.

F3 identifies ideals of $k[X]$ with ideals of R containing I(X). A corresponding pair is prime in one ring exactly when it is prime in the other: lift the two factors in the product test along the surjective quotient map; properness is also preserved. Thus step 2.1 is a strict inclusion-reversing bijection with primes of $k[X]$.

Reverse each finite chain through this bijection. Its length is unchanged, so the suprema of geometric and prime-chain lengths coincide by F4. If X is empty, I(X)=R and k[X] is the zero ring; both dimensions are $-\mathrm{\infty }$ under the stated extension.