Product Measures and Fubini's Theorem

Let $\mathcal G$ be the collection of $E$ whose every section lies in $\mathcal B$. A rectangle has section $(A\times B)_x=B$ if $x\in A$ and $\emptyset$ otherwise, both in $\mathcal B$, so $\mathcal G$ contains the rectangles. Sectioning commutes with set operations, $(E^c)_x=(E_x)^c$ and $(\bigcup_n E^{(n)})_x=\bigcup_n E^{(n)}_x$, so $\mathcal G$ is a sigma-algebra. It contains the generating rectangles, hence all of $\mathcal A\otimes\mathcal B$. The function statement follows by slicing a preimage, $(f_x)^{-1}(C)=(f^{-1}(C))_x$, which is measurable for Borel $C$.

Assume first $\nu(Y)<\infty$. Let $\mathcal D$ be the class of $E$ for which $x\mapsto\nu(E_x)$ is measurable. Rectangles lie in $\mathcal D$ since $\nu((A\times B)_x)=\nu(B)\mathbf 1_A(x)$. For disjoint $E,F\in\mathcal D$, additivity of $\nu$ on the disjoint sections gives $\nu((E\cup F)_x)=\nu(E_x)+\nu(F_x)$, a sum of measurable functions, so finite disjoint unions stay in $\mathcal D$, and the finite-measure case gives $\nu((E^c)_x)=\nu(Y)-\nu(E_x)$, so $\mathcal D$ is closed under complement. For an increasing sequence $E^{(n)}\uparrow E$ the sections rise, and continuity of $\nu$ from below makes $\nu(E_x)=\lim_n\nu(E^{(n)}_x)$ a pointwise limit of measurable functions, so $\mathcal D$ is closed under increasing limits. These properties make $\mathcal D$ a Dynkin system, while the rectangles are closed under intersection, $(A_1\times B_1)\cap(A_2\times B_2)=(A_1\cap A_2)\times (B_1\cap B_2)$, so they form a pi-system. Dynkin's pi-lambda theorem gives $\mathcal A\otimes\mathcal B\subseteq\mathcal D$. For general sigma-finite $\nu$, write $Y=\bigcup_k Y_k$ with $\nu(Y_k)<\infty$ and $Y_k$ increasing, apply the finite case to each $\nu(\,\cdot\cap Y_k)$, and let $k\to\infty$ using continuity from below.

By Lemma 3 both integrals are defined. Set $\rho(E)=\int_X\nu(E_x)\,d\mu$. Then $\rho(\emptyset)=0$, and for disjoint $E^{(n)}$ the sections are disjoint, so countable additivity of $\nu$ and the monotone convergence theorem give $\rho(\bigcup_n E^{(n)})=\int_X\sum_n\nu(E^{(n)}_x)\,d\mu=\sum_n\rho(E^{(n)})$, so $\rho$ is a measure. On a rectangle $\rho(A\times B)=\int_A\nu(B)\,d\mu=\mu(A)\nu(B)$. The symmetric integral defines a measure agreeing with $\rho$ on rectangles, and the rectangles form an intersection-closed generating system on which both measures are sigma-finite, so by the uniqueness of measures on a generating system the two integrals coincide and define the unique product measure.

For $f=\mathbf 1_E$ the inner integral is $\nu(E_x)$ and the identity is exactly Equation (1). Linearity extends it to nonnegative simple functions. A general nonnegative measurable $f$ is the increasing pointwise limit of simple functions $s_n\uparrow f$, and the monotone convergence theorem applied twice, once in the inner integral and once in the outer, carries the identity through the limit, the measurability of $x\mapsto\int_Y f_x\,d\nu$ surviving as a limit of measurable functions. The same argument in the other order gives the second equality.

Apply Theorem 5 to $\abs f$, which is integrable, so $\int_X\big(\int_Y\abs{f_x}\,d\nu \big)d\mu=\int\abs f\,d(\mu\otimes\nu)<\infty$. A nonnegative function with finite integral is finite almost everywhere, so $\int_Y\abs{f_x}\,d\nu<\infty$ for $\mu$-almost every $x$, that is $f_x$ is integrable for almost every $x$. Split $f=f^+-f^-$ into its nonnegative and nonpositive parts, each dominated by $\abs f$ and so integrable. Tonelli applies to $f^+$ and $f^-$ separately, and subtracting the two finite iterated integrals, legitimate because both are finite, gives the iterated integral of $f$ equal to $\int f^+\,d(\mu\otimes\nu)-\int f^-\,d(\mu\otimes\nu)=\int f\,d(\mu\otimes\nu)$. The other order is identical. For complex $f$ apply this to $\operatorname{Re}f$ and $\operatorname{Im}f$ separately, each integrable since $\abs{\operatorname{Re}f},\abs{\operatorname{Im}f}\le\abs f$, and recombine.