The normalization of an irreducible affine variety is finite

The coordinate ring $A=k[X]$ of the irreducible affine variety $X$ is a finite-type $k$-algebra and, by [L3] (applied to the nonempty variety $X$), an integral domain; hence $A$ is a finite-type domain over $k$. By [L1] the integral closure $B$ of $A$ in $\mathrm{Frac}(A)=k(X)$ is a finite $A$-module, and by [L6] $B$ is an integrally closed domain with $A\subseteq B\subseteq k(X)$ and $\mathrm{Frac}(B)=\mathrm{Frac}(A)=k(X)$ because $B$ was formed inside $k(X)$.

$B$ is a reduced affine $k$-algebra: it is a finite module over the finite-type $k$-algebra $A$, hence a finite-type $k$-algebra by [L2], and it is a domain by [L6], hence reduced. By [L2] there are $n\ge 0$ and an affine algebraic set $Y_0\subseteq {\mathbf{A}}_k^n$ with a $k$-algebra isomorphism $B\cong k[Y_0]$; the given variety $Y$ is one such, with $k[Y]\cong B$. Moreover $Y$ is nonempty: if $Y$ were empty, then by [L3] its vanishing ideal would be the unit ideal, so $k[Y]=0$, contradicting $B\cong k[Y]\mathrm{\ne }0$. Since $k[Y]$ is a domain, [L3] makes $Y$ a classical affine variety; and $k[Y]\cong B$ is integrally closed by [L6], so $Y$ is normal in the stated sense.

By [L4] the canonical bijection $\mathrm{Mor}(Y,X)\cong {\mathrm{Hom}}_{k\text{-alg}}(k[X],k[Y])$ implemented by pullback attaches to the composition $k[X]=A\hookrightarrow B\cong k[Y]$ a unique morphism $\nu :Y\to X$ with ${\nu }^{\ast }:k[X]\to k[Y]$ equal to that inclusion. This is clause 1, and it is the map induced by the inclusion of the coordinate ring in its integral closure.

$\nu$ is finite: $k[Y]\cong B$ is a finite $A=k[X]$-module by step 1.1, and the $k[X]$-module structure transported to $k[Y]$ along ${\nu }^{\ast }$ is the same structure, so $k[Y]$ is a finite $k[X]$-module. This is clause 4.

$\nu$ is birational and $k(X)\cong k(Y)$ as $k$-extensions: by [L5] the pullback ${\nu }^{\ast }:k(X)\to k(Y)$ is the homomorphism of function fields induced by the coordinate-ring pullback ${\nu }^{\ast }:A\to k[Y]$, that is, by the inclusion $A\hookrightarrow B$ followed by $B\cong k[Y]$. Under the identifications $k(X)=\mathrm{Frac}(A)$ and $k(Y)=\mathrm{Frac}(k[Y])\cong \mathrm{Frac}(B)=\mathrm{Frac}(A)$ of [L5] and step 1.1, this is the identity, an isomorphism of $k$-extensions. Hence $X$ and $Y$ are birationally equivalent by [L5]; and since the inverse isomorphism $k(Y)\to k(X)$ corresponds by [L5] to a dominant rational map $\theta :X⇢Y$, while the pullback of $\nu$ is invertible, the functoriality in [L5] gives $\theta \circ \nu ={\mathrm{id}}_Y$ and $\nu \circ \theta ={\mathrm{id}}_X$ as rational maps: the pullbacks of both sides agree, and the correspondence is injective. So $\nu$ is birational. This is clauses 2 (normality was settled in step 2.1) and 3.

The Axiom of Choice is used exactly through the published classical dictionary: as [L7] records, the object-level duality [L2], the variety/prime correspondence and Nullstellensatz [L3], the morphism anti-equivalence [L4] and the function-field correspondence [L5] that supply $Y$, the normality transport, birationality and the finiteness translation all reach the published axiom of choice (declared in the dependency list of this item). The module-finiteness theorem [L1] that makes $B$ a finite $A$-module is choice-free, so passing to the classical variety is the only place where choice is spent. Consequently the corollary holds under AC and states it explicitly; no smoothness or projectivity of $X$ or $Y$ is asserted or used.