[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$.
[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]
[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*}
[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]
[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]
