Tensor products of operator matrix units form a basis

For a product basis vector $e_{v^{\mathrm{\prime }}}\otimes f_{t^{\mathrm{\prime }}}$, [F3] gives $(E_{uv}\otimes F_{st})(e_{v^{\mathrm{\prime }}}\otimes f_{t^{\mathrm{\prime }}})=e_u\otimes f_s$ when $v^{\mathrm{\prime }}=v$ and $t^{\mathrm{\prime }}=t$, and gives $0$ otherwise, by orthonormality in [F1]. Thus each tensor matrix unit has a single coordinate $1$ and zeros elsewhere in the product basis.

Every endomorphism $T$ of $H\otimes H^{\mathrm{\prime }}$ has a unique coordinate coefficient $c_{(u,s),(v,t)}$ for the image of each product basis vector $e_v\otimes f_t$. The finite sum ${\sum }_{u,s,v,t}{c}_{(u,s),(v,t)}{E}_{uv}\otimes F_{st}$ has the same image as $T$ on each such basis vector by step 1.1; [F4] therefore makes it equal to $T$. The same coordinate entries show that this expression is unique. If $n=0$ or $m=0$, the product space is zero by [F2] and both the basis and sum are empty.