A Theorem by Von Neumann, which pertains a product of two Hilbert Spaces 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: 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.
A: Since no one noticed, I feel I should point out that OP's actual statement of the theorem is incorrect. It might not be possible to match up the two bases, for instance you could have the sum $\sum 2^{-n}e_n\otimes e_{n+1}$. It's impossible to reindex the two bases to get this in the form $\sum 2^{-n} e_n\otimes f_n$ because there's an element of the second basis that doesn't get paired with any element of the first basis.
(There's also the nitpick that he assumed $\omega$ is a unit vector, but that's less interesting.)
