Corollary 1

— For $1 \leq i \leq n$, let $(e_{i,\alpha})_{\alpha \in A(i)}$ be an orthonormal basis of $E_i$. Then the family of vectors $e_{1,\alpha_1} \otimes \ldots \otimes e_{n,\alpha_n}$ as $(\alpha_1, \ldots, \alpha_n)$ ranges over $A(1) \times \cdots \times A(n)$ is an orthonormal basis of $E_1 \hat{\otimes}_2 \ldots \hat{\otimes}_2 E_n$.