Counting-measure integration is a nonnegative series

For each integer $m\ge 1$, define $s_m(n)=\min \{f(n),m\}$ when $n<m$ and $s_m(n)=0$ when $n\ge m$. Every subset of $\mathbb{N}$ is measurable under [F1], so $s_m$ is measurable; its range is finite, hence it is simple by [F2]. For fixed $n$, the indicator $1_{n<m}$ is eventually one; if $f(n)<+\mathrm{\infty }$, [F5] ensures the increasing canonical naturals eventually exceed $f(n)$, while if $f(n)=+\mathrm{\infty }$ the capped values increase without bound. Thus $s_m(n)\uparrow f(n)$ for every $n$. Monotone convergence [F3] gives $\int fd\mathrm{\#}={\lim }_{m\to \mathrm{\infty }}\int s_{m}d\mathrm{\#}$.

By [F1] and [F2], for every $m\ge 1$, $\int s_{m}d\mathrm{\#}={\sum }_{n<m}\min \{f(n),m\}\mathrm{\#}(\{n\})={\sum }_{n<m}\min \{f(n),m\}=:D_m\mathrm{.}$ For each $n<m$, $\min \{f(n),m\}\le \min \{f(n),m+1\}$ and $D_{m+1}$ adds a nonnegative term, so $D_m$ is nondecreasing. Termwise $\min \{f(n),m\}\le f(n)$, so $D_m\le P_m\le {\sum }_{n=0}^{\mathrm{\infty }}f(n)$ by [F4].

Fix $r\ge 0$. If $P_r=+\mathrm{\infty }$, some $f(n)=+\mathrm{\infty }$ with $n<r$, so for every $m\ge r$ with $m>n$, $D_m\ge m$; the canonical naturals are unbounded by [F5], hence ${\lim }_m{D}_m=+\mathrm{\infty }\ge P_r$. If $P_r<+\mathrm{\infty }$, then each $f(n)$ for $n<r$ is finite. Write $\bar{r}=r\cdot 1_{\mathbb{R}}$ and apply [F5] to $P_r+\bar{r}$ to choose an integer $m$ with $m\cdot 1_{\mathbb{R}}>P_r+\bar{r}$. Then $m\ge r$ and $m>f(n)$ for every $n<r$, since nonnegative summands give $f(n)\le P_r$. Thus $D_m\ge P_r$, and monotonicity of $D_m$ again gives ${\lim }_m{D}_m\ge P_r$. Since this holds for every $r$, [F4] implies ${\lim }_m{D}_m\ge {\sum }_{n=0}^{\mathrm{\infty }}f(n)$. Together with step 2.1's reverse bound, ${\lim }_m{D}_m={\sum }_{n=0}^{\mathrm{\infty }}f(n)$.

Steps 1.1 and 2.1 identify the integral with ${\lim }_m{D}_m$, and step 3.1 identifies that limit with the nonnegative extended series. This proves the stated identity, including infinite values.