This thread is just a note.
Given Hilbert spaces.
Consider their hilbertian tensor product: $$\mathcal{H}\hat{\otimes}\mathcal{K}:\quad\langle\varphi\otimes\psi,\varphi'\otimes\psi'\rangle:=\langle\varphi,\varphi'\rangle\langle\psi,\psi'\rangle$$
Then their ONB give rise to an ONB: $$\mathcal{S}\otimes\mathcal{T}:=\{\sigma\otimes\tau:\sigma\in\mathcal{S},\tau\in\mathcal{T}\}$$ How to prove this circumventing double-series?
This answer is community wiki.
Orthonormality follows immediately: $$\langle\sigma\otimes\tau,\sigma'\otimes\tau'\rangle=\langle\sigma,\sigma'\rangle\langle\tau,\tau'\rangle=\delta_{\sigma\sigma'}\delta_{\tau\tau'}$$ Totality follows from Parseval's inequality: $$\sum_{\sigma\tau}|\langle\varphi\otimes\psi,\sigma\otimes\tau\rangle|^2=\sum_\sigma|\langle\varphi,\sigma\rangle|^2\sum_\tau|\langle\psi,\tau\rangle|^2=\|\varphi\|^2\|\psi\|^2=\|\varphi\otimes\psi\|^2$$ But the span of simple tensors is dense.