Solution (source code)

= Solution

The <monotone convergence theorem> states that if $0\leq h_n\uparrow h$ pointwise for measurable <functions>, then $h$ is measurable and $\int h=\lim_n\int h_n$, allowing infinity.

Apply it to the partial sums $S_N=\sum_{n=0}^Nf_n$. They are nonnegative, measurable, and increase pointwise to $f$. Finite additivity of the <integral> and monotone convergence yield
$$
\boxed{\int_{\mathbb R}f=\lim_{N\to\infty}\sum_{n=0}^N\int_{\mathbb R}f_n
=\sum_{n=0}^{\infty}\int_{\mathbb R}f_n.}
$$
The assumed finite sum of <integrals> makes $f$ integrable. This proves the series-integration rule needed below directly from the stated theorem, without assuming an additional interchange theorem.