The tensor product of two vector spaces V,W over \mathbb{F} is a vector space V \otimes W over \mathbb{F} together with a bilinear map V \times W \stackrel{\otimes}{\rightarrow} V \otimes W with the property that whenever \mathcal{B}_V, \mathcal{B}_W are bases for V,W respectively, the set \{ v_i \otimes w_j \mid v_i \in \mathcal{B}_V, w_j \in \mathcal{B}_W \} gives a basis for V \otimes W.
The following theorem shows that the property in the definition need not be checked for all pairs of bases; just one pair is sufficient.
Theorem: Let Y be a vector space and \phi : V \times W \rightarrow Y be bilinear. Suppose there are bases \mathcal{B}_V, \mathcal{B}_W for V,W respectively, such that \phi(v \times w) is a basis for Y. Then the same holds for any pair of bases.
Let V, W be vector spaces over \mathbb{F}. Following (Zakharevich 2015), our goal is to construct a vector space V \otimes W such that for any vector space Z,
\mathcal{L}(V \otimes W, Z) \cong
\big\{ \substack{\text{bilinear maps}\\{V \times W \rightarrow Z}} \big\}
Let A = \mathrm{Free}(V \times W) be the free vector space over \mathbb{F} on the product V \times W. We will demonstrate that
\mathcal{L}(A,Z) \cong \big\{ \substack{\text{functions}\\{V \times W \rightarrow Z}} \big\}
For v \in V, w \in W, define the notation v \otimes w \equiv \mathbb{1}_{(v,w)} \in A. A typical vector has the form f = \sum_{k=1}^n \alpha_k (v_k \otimes w_k) \in A. By linearity, observe that each T \in \mathcal{L}(A,Z) is determined uniquely by its values on the standard basis, exposing a bijection between \mathcal{L}(A,Z) and (nonlinear) functions V \times W \rightarrow Z.
T f
= T \left( \sum_{k=1}^n \alpha_k (v_k \otimes w_k) \right)
= \sum_{k=1}^n \alpha_k T (v_k \otimes w_k)
Step 2: Since \mathcal{L}(A,Z) represents arbitrary functions, we will construct V \oplus W by shrinking A so that \mathcal{L}(V \times W, Z) represents only the bilinear maps V \times W \rightarrow Z. For example, if T \in \mathcal{L}(V \otimes W, Z) is a linear map, the following proof of bilinearity in the first argument
\begin{aligned}
T( (v_1 + v_2) \otimes w )
&= T( (v_1 \otimes w) + (v_2 \otimes w) ) \\
&= T(v_1 \otimes w) + T(v_2 \otimes w)
\end{aligned}
requires that (v_1 + v_2) \otimes w and (v_1 \otimes w) + (v_2 \otimes w) refer to the same element in V \otimes W. Starting from A, we can enforce this equivalence implicitly by defining V \otimes W to be the quotient space A / A_0, where
A_0 = \mathrm{Span}\left\{
\begin{aligned}[c]
(v_1 + v_2) \otimes w - (v_1 \otimes w) - (v_2 \otimes w) \\
v \otimes (w_1 + w_2) - (v \otimes w_1) - (v \otimes w_2) \\
(\alpha v) \otimes w - \alpha (v \otimes w) \\
v \otimes (\alpha w) - \alpha (v \otimes w)
\end{aligned}
\;\middle\vert\;
\begin{array}{l}
\alpha \in F \\ v \in V, w \in W
\end{array}
\right\}
This choice was made so that each linear map T \in \mathcal{L}(V \otimes W, Z) will satisfy
\begin{aligned}
T( (v_1 + v_2) \otimes w) &= T(v_1 \otimes w) + T(v_2 \otimes w) \\
T( v \otimes (w_1 + w_2)) &= T(v \otimes w_1) + T(v \otimes w_2) \\
T( (\alpha v) \otimes w ) &= T( \alpha ( v \otimes w) ) \\
T( v \otimes (\alpha w) ) &= T( \alpha ( v \otimes w) )
\end{aligned}
(Technically, (v \otimes w) \in V \otimes W stands for the equivalence class of v \otimes w = \mathbb{1}_{(v,w)} \in A.)
As pointed out by Purbhoo 2012, since A = \mathrm{Free}(V \times W) is the space of formal linear combinations of (v,w) pairs, A_0 is the space of those linear combinations that can be simplified to the zero vector using bilinearity. Accordingly, A / A_0 reduces A to a space where two expressions are equal iff one can be simplified to the other using bilinearity.