I'm writing my thesis on the EPR paradox (I want to continue my master degree in physics) but I'm having an unusual problem. One passage from the book I'm following at the moment justifies one important passage saying that "a theorem proven by Von Neumann tells us" but, since it is far from obvious, I'd like to check the proof for some insight on the matter. The problem is: Von Neumann worked in a lot of fields, so I'm having a hard time figuring out which theorem is this. Any research failed me. It would be most helpful if someone recognized the result and pointed me in the right direction for a proof.
So, without further ado here is the theorem as it is used in the book: let $H\_1$ and $H\_2$ be two Hilbert spaces (separable as it is common usage in QM, so we are treating with the space of square integrable functions) and let us have two complete basis of orthonormal states $\phi\_i$ and $\psi\_j$, one for each space. Let $\omega$ be an element of the direct product of these two spaces. The most general way to express $\omega$ would be $$
\omega=\Sigma\_{i,j}c\_{ij}\phi\_i\psi\_j,
$$
where $\Sigma\_{i,j}|c\_{ij}|^2=1$. Now the theorem by Von Neumann says that we can find two other basis for $H\_1$ and $H\_2$ which I will denote by $\alpha\_i$ and $\beta\_j$ such that
$$
\omega=\Sigma\_i c\_i\alpha\_i\beta\_i,
$$
where of course $\Sigma\_i|c\_i|^2=1$.
I apologize for my messy writing but I'm kinda technologically impaired, I hope you still managed to get the idea. Basically, it allows us to have a sum over one single index.
As I said earlier, I don't want to bother too much so I don't ask for a proof, just for a nudge in the right direction. Thank you!



A Theorem by Von Neumann, which pertains a product of two Hilbert Spaces
As noted by Dan Stahlke, this is precisely the singular value decompositon for compact (in this case Hilbert-Schmidt) operators, via the identification of an element $\omega$ of the Hilbert space tensor product $H\_1\otimes H\_2$ with such an operator $T$. The result can be deduced from the spectral theorem for the compact operator $T^\ast T$ just as in the finite dimensional case.


Edit after Nik Weaver's answer. The correct statement of the result should talk about orthonormal sequences rather than bases.


