[proofplan] We show the set $\{e_i \otimes f_j\}$ is a basis for $V \otimes_k W$ by verifying two properties: spanning and linear independence. The spanning property follows from bilinearity of the tensor product, which reduces every elementary tensor $v \otimes w$ to a linear combination of $e_i \otimes f_j$, and then extends to all of $V \otimes_k W$ by linearity. Linear independence is established by constructing, for each pair $(i_0, j_0)$, a bilinear form whose induced linear functional on $V \otimes_k W$ vanishes on every $e_i \otimes f_j$ except $e_{i_0} \otimes f_{j_0}$. [/proofplan]

[step:Reduce every element of $V \otimes_k W$ to a linear combination of $e_i \otimes f_j$]By the [universal property of the tensor product](/theorems/???), every element of $V \otimes_k W$ is a finite sum of elementary tensors $v \otimes w$ with $v \in V$, $w \in W$. Fix such an elementary tensor. Since $\{e_1, \ldots, e_m\}$ is a basis for $V$ and $\{f_1, \ldots, f_n\}$ is a basis for $W$, write \begin{align*} v = \sum_{i=1}^m a_i e_i, \qquad w = \sum_{j=1}^n b_j f_j, \end{align*} with $a_i, b_j \in k$. Bilinearity of the tensor product gives \begin{align*} v \otimes w = \left(\sum_{i=1}^m a_i e_i\right) \otimes \left(\sum_{j=1}^n b_j f_j\right) = \sum_{i=1}^m \sum_{j=1}^n a_i b_j \, (e_i \otimes f_j). \end{align*} Since every element of $V \otimes_k W$ is a finite sum of elementary tensors, and each elementary tensor is a linear combination of $\{e_i \otimes f_j\}$, the set $\{e_i \otimes f_j : 1 \le i \le m, 1 \le j \le n\}$ spans $V \otimes_k W$.[/step]

[guided]We need to show that $\{e_i \otimes f_j\}$ spans $V \otimes_k W$. By the [universal property of the tensor product](/theorems/???), every element of $V \otimes_k W$ is a finite sum of elementary tensors $v \otimes w$. So it suffices to show that each elementary tensor $v \otimes w$ lies in $\operatorname{span}\{e_i \otimes f_j\}$. Fix $v \in V$ and $w \in W$. Since $\{e_1, \ldots, e_m\}$ is a basis for $V$ and $\{f_1, \ldots, f_n\}$ is a basis for $W$, there exist unique scalars $a_i, b_j \in k$ with \begin{align*} v = \sum_{i=1}^m a_i e_i, \qquad w = \sum_{j=1}^n b_j f_j. \end{align*} The tensor product is bilinear: it is linear in each factor when the other is held fixed. Applying linearity in the first factor (with $w$ fixed), then linearity in the second factor (with each $e_i$ fixed): \begin{align*} v \otimes w = \left(\sum_{i=1}^m a_i e_i\right) \otimes w = \sum_{i=1}^m a_i\, (e_i \otimes w) = \sum_{i=1}^m a_i \left(e_i \otimes \sum_{j=1}^n b_j f_j\right) = \sum_{i=1}^m \sum_{j=1}^n a_i b_j\, (e_i \otimes f_j). \end{align*} Every elementary tensor is therefore a linear combination of the $mn$ elements $e_i \otimes f_j$, and since every element of $V \otimes_k W$ is a finite sum of elementary tensors, the set $\{e_i \otimes f_j\}$ spans $V \otimes_k W$.[/guided]

[step:Construct coordinate functionals on $V \otimes_k W$ via the universal property]For each pair $(i_0, j_0)$ with $1 \le i_0 \le m$ and $1 \le j_0 \le n$, define the bilinear form \begin{align*} \beta_{i_0, j_0}: V \times W &\to k \\ (v, w) &\mapsto \varepsilon_{i_0}(v) \cdot \varepsilon_{j_0}'(w), \end{align*} where $\varepsilon_{i_0}: V \to k$ is the $i_0$-th coordinate functional with respect to the basis $\{e_1, \ldots, e_m\}$ (so $\varepsilon_{i_0}(e_i) = \delta_{i, i_0}$), and $\varepsilon_{j_0}': W \to k$ is the $j_0$-th coordinate functional with respect to $\{f_1, \ldots, f_n\}$ (so $\varepsilon_{j_0}'(f_j) = \delta_{j, j_0}$). The map $\beta_{i_0, j_0}$ is bilinear because it is the product of two linear functionals. By the [universal property of the tensor product](/theorems/???), there exists a unique linear map \begin{align*} \tilde{\beta}_{i_0, j_0}: V \otimes_k W \to k \end{align*} satisfying $\tilde{\beta}_{i_0, j_0}(v \otimes w) = \varepsilon_{i_0}(v) \cdot \varepsilon_{j_0}'(w)$ for all $v \in V$, $w \in W$. Evaluating on basis tensors: \begin{align*} \tilde{\beta}_{i_0, j_0}(e_i \otimes f_j) = \delta_{i, i_0}\, \delta_{j, j_0}. \end{align*}[/step]

[guided]To prove linear independence, we need a way to "read off" the coefficient of each $e_i \otimes f_j$ in a linear combination. The strategy is to construct, for each pair $(i_0, j_0)$, a linear functional on $V \otimes_k W$ that extracts the $(i_0, j_0)$-coefficient. For each $1 \le i_0 \le m$, let $\varepsilon_{i_0}: V \to k$ denote the $i_0$-th coordinate functional defined by $\varepsilon_{i_0}(e_i) = \delta_{i, i_0}$ (the Kronecker delta). This is the unique element of $V^*$ satisfying $\varepsilon_{i_0}\left(\sum_i a_i e_i\right) = a_{i_0}$. Similarly, for each $1 \le j_0 \le n$, let $\varepsilon_{j_0}': W \to k$ be the $j_0$-th coordinate functional with $\varepsilon_{j_0}'(f_j) = \delta_{j, j_0}$. Now define \begin{align*} \beta_{i_0, j_0}: V \times W &\to k \\ (v, w) &\mapsto \varepsilon_{i_0}(v) \cdot \varepsilon_{j_0}'(w). \end{align*} This is bilinear: for fixed $w$, the map $v \mapsto \varepsilon_{i_0}(v) \cdot \varepsilon_{j_0}'(w)$ is linear because $\varepsilon_{i_0}$ is linear and $\varepsilon_{j_0}'(w)$ is a scalar, and symmetrically in the second argument. By the [universal property of the tensor product](/theorems/???), there is a unique linear map $\tilde{\beta}_{i_0, j_0}: V \otimes_k W \to k$ satisfying \begin{align*} \tilde{\beta}_{i_0, j_0}(v \otimes w) = \beta_{i_0, j_0}(v, w) = \varepsilon_{i_0}(v) \cdot \varepsilon_{j_0}'(w) \end{align*} for all $v \in V$, $w \in W$. Why does this help? Because evaluating on basis tensors gives \begin{align*} \tilde{\beta}_{i_0, j_0}(e_i \otimes f_j) = \varepsilon_{i_0}(e_i) \cdot \varepsilon_{j_0}'(f_j) = \delta_{i, i_0}\, \delta_{j, j_0}, \end{align*} so $\tilde{\beta}_{i_0, j_0}$ picks out the coefficient of $e_{i_0} \otimes f_{j_0}$ and kills all other basis tensors.[/guided]

[step:Deduce linear independence from the coordinate functionals] Suppose \begin{align*} \sum_{i=1}^m \sum_{j=1}^n c_{ij}\, (e_i \otimes f_j) = 0 \end{align*} for some scalars $c_{ij} \in k$. Applying the linear functional $\tilde{\beta}_{i_0, j_0}$ constructed in the previous step to both sides: \begin{align*} 0 = \tilde{\beta}_{i_0, j_0}\!\left(\sum_{i,j} c_{ij}\, (e_i \otimes f_j)\right) = \sum_{i,j} c_{ij}\, \tilde{\beta}_{i_0, j_0}(e_i \otimes f_j) = \sum_{i,j} c_{ij}\, \delta_{i, i_0}\, \delta_{j, j_0} = c_{i_0 j_0}. \end{align*} Since $(i_0, j_0)$ was arbitrary, $c_{ij} = 0$ for all $1 \le i \le m$ and $1 \le j \le n$. Therefore $\{e_i \otimes f_j\}$ is linearly independent. [/step]

[step:Conclude the dimension formula] Since $\{e_i \otimes f_j : 1 \le i \le m, 1 \le j \le n\}$ is a spanning set (by the first step) and linearly independent (by the third step), it is a basis for $V \otimes_k W$. The number of elements in this basis is $mn = \dim(V) \cdot \dim(W)$, so \begin{align*} \dim(V \otimes_k W) = \dim(V) \cdot \dim(W). \end{align*} [/step]