Applying results

(i)	R4551: Expressing a finite composition of indicator function and measure-preserving transformation in terms of set cardinality
(ii)	R1868: Composition of indicator function with set endomorphism
(iii)	R4549:
(iv)	R2089: Unsigned basic expectation is compatible with probability measure

we have \begin{equation} \begin{split} \lim_{N \to \infty} \frac{\# \{ n \in \{ 0, \ldots, N - 1 \} : T^n \in E \}}{N} & = \lim_{N \to \infty} \frac{1}{N} \sum_{n = 0}^{N - 1} I_{T^{-n} E} \\ & = \lim_{N \to \infty} \frac{1}{N} \sum_{n = 0}^{N - 1} (I_E \circ T^n) \overset{a.s.}{=} \mathbb{E} (I_E) = \mathbb{P}(E) \end{split} \end{equation} $\square$