The product of affine varieties has coordinate ring k[X] tensor_k k[Y]

Put $A=k[X]$, $B=k[Y]$, and $C=A{\otimes }_{k}B$. The prime-coordinate-ring criterion makes $A$ and $B$ domains. The algebra $C$ is finitely generated by generators of $A$ tensored with $1$ and elements $1\otimes b$ for generators $b$ of $B$. To prove it is a domain, take nonzero $c={\sum }_i{a}_i\otimes b_i$ and $d={\sum }_j{a}_j^{\mathrm{\prime }}\otimes b_j^{\mathrm{\prime }}$, choosing the $b_i$ linearly independent and, separately, the $b_j^{\mathrm{\prime }}$ linearly independent, with $a_1,a_1^{\mathrm{\prime }}\mathrm{\ne }0$. Since $A$ is a domain, $a_1{a}_1^{\mathrm{\prime }}$ is a nonzero function on $X$, so it is nonzero at some $x\in X$. Evaluation in the first factor sends $c,d$ to nonzero elements of $B$ by linear independence. Their product is nonzero because $B$ is a domain; therefore $cd\mathrm{\ne }0$ in $C$. Also $1\otimes 1\mathrm{\ne }0$ over the field $k$. Hence $C$ is a nonzero reduced affine $k$-algebra.

Now thm-affine-algebraic-sets-coordinate-duality constructs an affine algebraic set $Z$ with coordinate algebra $C$. It is nonempty, since the empty set has zero coordinate ring, whereas $C\mathrm{\ne }0$. Since $C$ is a domain, thm-affine-variety-prime-coordinate-ring makes $Z$ a classical affine variety. Only now apply thm-affine-morphisms-coordinate-ring-anti-equivalence: the two canonical maps $A\to C$, $B\to C$ give morphisms $p:Z\to X$, $q:Z\to Y$.

For a classical affine variety $T$ and morphisms $f:T\to X$, $g:T\to Y$, the tensor coproduct theorem gives a unique $k$-algebra map $C\to k[T]$ extending $f^{\ast }$ and $g^{\ast }$. Since $T$ and $Z$ are now both classical affine varieties, the affine morphism correspondence turns this into the unique morphism $T\to Z$ with projections $f,g$. This is the required universal property, and $k[Z]=C$ proves the ring formula. If a factor is a point, its ring is $k$ and the same argument gives $A{\otimes }_{k}k\cong A$.