[proofplan] We construct the homomorphism from the [universal property of the tensor product](/theorems/3971) and then prove it is surjective and injective directly as a map of polynomial functions. Surjectivity follows because the coordinate functions on $X\times Y$ come from the coordinate functions on $X$ and $Y$. Injectivity is proved by reducing a finite tensor expression to one whose second factors are $k$-linearly independent functions on $Y$, and then evaluating at each point of $X$. [/proofplan]

[step:Construct the induced algebra homomorphism on the tensor product] For $f\in k[X]$ and $g\in k[Y]$, choose polynomial representatives $F\in k[x_1,\dots,x_n]$ and $G\in k[y_1,\dots,y_m]$. Define the polynomial $H\in k[x_1,\dots,x_n,y_1,\dots,y_m]$ by $H(x,y)=F(x)G(y)$. Its restriction to $X\times Y$ depends only on the classes $f$ and $g$, so it defines a regular function $\mu(f,g):X\times Y\to k$ by \begin{align*} \mu(f,g)(p,q)=f(p)g(q). \end{align*} Pointwise addition and multiplication in coordinate rings show that $\mu$ is $k$-bilinear. Therefore, by the defining universal property of the [tensor product](/page/Tensor%20Product), $\mu$ induces a unique $k$-[linear map](/page/Linear%20Map) $\Phi:k[X]\otimes_k k[Y]\to k[X\times Y]$ such that \begin{align*} \Phi(f\otimes g)(p,q)=f(p)g(q) \end{align*} for all $f\in k[X]$, $g\in k[Y]$, and $(p,q)\in X\times Y$. Moreover, $\Phi$ is a $k$-algebra homomorphism. Indeed, for pure tensors $f_1\otimes g_1$ and $f_2\otimes g_2$, \begin{align*} \Phi((f_1\otimes g_1)(f_2\otimes g_2))(p,q)=f_1(p)f_2(p)g_1(q)g_2(q). \end{align*} The same expression equals \begin{align*} \Phi(f_1\otimes g_1)(p,q)\Phi(f_2\otimes g_2)(p,q). \end{align*} By bilinearity this proves multiplicativity on all of $k[X]\otimes_k k[Y]$, and $\Phi(1\otimes 1)=1$. [/step]

[step:Show the map is surjective from the coordinate generators]Let $\bar x_i\in k[X]$ denote the restriction of the coordinate function $x_i$ to $X$, and let $\bar y_j\in k[Y]$ denote the restriction of the coordinate function $y_j$ to $Y$. In $k[X\times Y]$, the coordinate functions are \begin{align*} (p,q)&\mapsto p_i \end{align*} for $1\le i\le n$, and \begin{align*} (p,q)&\mapsto q_j \end{align*} for $1\le j\le m$. These coordinate functions lie in the image of $\Phi$, since \begin{align*} \Phi(\bar x_i\otimes 1)(p,q)=p_i \end{align*} and \begin{align*} \Phi(1\otimes \bar y_j)(p,q)=q_j. \end{align*} By the coordinate-ring description of $X\times Y$ in the theorem statement, the coordinate ring $k[X\times Y]$ is generated as a $k$-algebra by these coordinate functions. Since the image of a $k$-algebra homomorphism is a $k$-subalgebra, it contains every polynomial expression in them. Hence $\Phi$ is surjective.[/step]

[guided]The point of this step is that no separate computation of the ideal of $X\times Y$ is needed for surjectivity. The coordinate ring $k[X\times Y]$ is, by definition, the algebra of polynomial functions on $X\times Y$, so it is generated by the restrictions of the ambient coordinate functions. For each $1\le i\le n$, let $\bar x_i\in k[X]$ be the function $p\mapsto p_i$. Then \begin{align*} \Phi(\bar x_i\otimes 1)(p,q)=\bar x_i(p)\cdot 1=p_i. \end{align*} Thus the $x_i$-coordinate function on $X\times Y$ belongs to the image of $\Phi$. Similarly, for each $1\le j\le m$, let $\bar y_j\in k[Y]$ be the function $q\mapsto q_j$. Then \begin{align*} \Phi(1\otimes \bar y_j)(p,q)=1\cdot \bar y_j(q)=q_j. \end{align*} Thus the $y_j$-coordinate function on $X\times Y$ also belongs to the image. Because every element of $k[X\times Y]$ is represented by a polynomial in the coordinate functions $x_1,\dots,x_n,y_1,\dots,y_m$, every element of $k[X\times Y]$ is a polynomial expression in functions already lying in the image of $\Phi$. The image is closed under addition, scalar multiplication, and multiplication because $\Phi$ is a $k$-algebra homomorphism. Therefore every element of $k[X\times Y]$ lies in the image of $\Phi$, so $\Phi$ is surjective.[/guided]

[step:Prove injectivity by evaluating against linearly independent functions on $Y$] Let $u\in k[X]\otimes_k k[Y]$ satisfy $\Phi(u)=0$. Since tensors are finite sums, the second factors appearing in any expression for $u$ span a finite-dimensional $k$-subspace of $k[Y]$. Choose a $k$-basis $b_1,\dots,b_r$ of that subspace and rewrite the original expression in this basis. Thus there are elements $a_1,\dots,a_r\in k[X]$ such that \begin{align*} u=\sum_{\ell=1}^r a_\ell\otimes b_\ell, \end{align*} and $b_1,\dots,b_r$ are $k$-linearly independent. For every $p\in X$ and $q\in Y$, the equality $\Phi(u)=0$ gives \begin{align*} \sum_{\ell=1}^r a_\ell(p)b_\ell(q)=0. \end{align*} Fix $p\in X$. The function $Y\to k$ defined by $q\mapsto \sum_{\ell=1}^r a_\ell(p)b_\ell(q)$ is the zero element of $k[Y]$. Since $b_1,\dots,b_r$ are $k$-linearly independent in $k[Y]$, all coefficients vanish: \begin{align*} a_\ell(p)=0 \end{align*} for every $1\le \ell\le r$. Because this holds for every $p\in X$, each $a_\ell$ is the zero element of $k[X]$ as a polynomial function on $X$. If $X=\varnothing$, the same conclusion holds because all polynomial functions on $X$ are the unique function $\varnothing\to k$, so $k[X]$ is the zero $k$-algebra under the stated convention. Hence \begin{align*} u=\sum_{\ell=1}^r 0\otimes b_\ell=0. \end{align*} Thus $\ker\Phi=\{0\}$, so $\Phi$ is injective. [/step]

[step:Identify the isomorphism with the stated bilinear formula] The map $\Phi$ is a bijective $k$-algebra homomorphism, hence an isomorphism of $k$-algebras. By its construction from the tensor product universal property, it satisfies \begin{align*} \Phi(f\otimes g)(p,q)=f(p)g(q) \end{align*} for all $f\in k[X]$, $g\in k[Y]$, and $(p,q)\in X\times Y$. Therefore the original $k$-bilinear map induces precisely the claimed isomorphism \begin{align*} k[X]\otimes_k k[Y]\cong k[X\times Y]. \end{align*} [/step]