I saw in several texts, as a part of the spectral theorem for unitary operators, that given a unitary operator $U$ on a Hilbert space $H$ (say it is separable), $H$ can be decomposed as an orthogonal direct sum (finite or countable) of cyclic sub-spaces (i.e. spaces of the form $\operatorname{cls}(\operatorname{span}\{U^nx/n\in\mathbb{Z}\})$ for some vector $x$).
I couldn't find a proof for that, so if someone could give me a reference or a sketch of the proof it would be great.
