Classical affine algebraic sets and reduced finitely generated $k$-algebras are contravariantly equivalent

For every algebraic set $X$, F1 places $k[X]$ in the proposed algebra category, and F4 makes pullback a contravariant functor that is bijective on every hom-set. Thus it is fully faithful, including the empty cases already verified there.

Given a reduced finite-type algebra $B$, choose a surjective presentation $R=k[T_1,\dots ,T_m]\to B$ with kernel $J$. If $h^r\in J$ for $r\ge 1$, the image of $h$ is nilpotent and hence zero by reducedness, so $h\in J$. Therefore $J$ is radical. F3 gives $I(V(J))=J$, and the presentation identifies $k[V(J)]=R\mathrm{/}J$ with $B$. For $B=0$, $J=R$ and $V(J)=\mathrm{\varnothing }$.

The object realization can be made intrinsic: use the maximal ideals of $B$, with the topology and regular functions transported from any presentation. F5 identifies the points, and the algebra isomorphism between two presentations gives inverse morphisms by F4. Their pullbacks are the prescribed identities on $B$, so full faithfulness forces all such comparison maps and their composites to agree. Thus the realization is independent up to canonical isomorphism, and step 1.1 with step 1.2 proves the antiequivalence.