Conditional integration through a regular conditional law

For $f={\mathbf{1}}_A$, the assertion is [F1]. If $f={\sum }_{j=1}^m{a}_j{\mathbf{1}}_{A_j}$ is nonnegative simple with disjoint measurable $A_j$ and finite coefficients, then $I_f={\sum }_j{a}_{j}K(\cdot ,A_j)$, so finite additivity of integrals proves the identity by summing the indicator identities. It includes the empty sum, giving $I_0=0$, and $f=1$, giving $I_1=1$.

For general nonnegative $f$, choose the prescribed simple approximants $s_n\uparrow f$ of [F4]. For every $\omega$, [F3] for the probability $K(\omega ,\cdot )$ gives $I_{s_n}(\omega )\uparrow I_f(\omega )$. The function $(\omega ,x)\mapsto f(x)$ is product-measurable since inverse images are $\mathrm{\Omega }\times f^{-1}(B)$; thus [F2] ensures $\mathcal{G}$-measurability of $I_f$. Applying [F3] on each $H$ on both sides of step 1.1 proves the displayed identity, allowing infinity. No representative selection or AC occurred. If using conditional-class notation, [F5] identifies this characterized nonnegative function with the class, under [F7].

For real $f$ with $C=E\mathrm{\mid }f(X)\mathrm{\mid }<\mathrm{\infty }$, step 2.1 at $\mathrm{\mid }f\mathrm{\mid }$ and $H=\mathrm{\Omega }$ gives $\int I_{\mathrm{\mid }f\mathrm{\mid }}dP=C$. Also $C=\int \mathrm{\mid }f\mathrm{\mid }d{P}_X$ by [F8], checking the equivalent law integrability condition. The set $D=\{I_{\mathrm{\mid }f\mathrm{\mid }}<\mathrm{\infty }\}$ is measurable. For every positive integer $n$, $nP(D^c)\le \int I_{\mathrm{\mid }f\mathrm{\mid }}=C$, hence $P(D^c)=0$. On $D$, both $I_{f^{+}},I_{f^{-}}$ are finite and their difference $J$ is the signed integral. Fill $J$ by zero off $D$; it is real measurable by [F2], and $\mathrm{\mid }J\mathrm{\mid }\le I_{\mathrm{\mid }f\mathrm{\mid }}$ on $D$, so $J$ is integrable. The two nonnegative identities from step 2.1 have finite integrals, at most $C$, so subtraction gives ${\int }_{H}JdP={\int }_{H}f(X)dP$. Removing $D^c$ changes neither integral, since it is measurable null. Thus $J$ is a conditional version; [F6] gives its almost-sure uniqueness, and [F7] supplies only the inherited class notation. No infinity is subtracted from infinity.