[proofplan] The proof is a four-stage bootstrap. We first verify the iterated integral identity for indicators of measurable rectangles (direct computation), then extend to indicators of all product-measurable sets via the [Dynkin $\pi$-system lemma](/theorems/505), pass to non-negative measurable functions via simple-function approximation and the [Monotone Convergence Theorem](/theorems/509), and finally handle integrable functions by splitting $f = f^+ - f^-$. At each stage, the measurability of sections and of the inner integral must be verified. [/proofplan] [step:Verify the identity for indicators of measurable rectangles by direct computation] For $A_1 \in \mathcal{E}_1$ and $A_2 \in \mathcal{E}_2$, define $f = \mathbb{1}_{A_1 \times A_2}$. For fixed $x_1 \in E_1$, the section $x_2 \mapsto \mathbb{1}_{A_1 \times A_2}(x_1, x_2) = \mathbb{1}_{A_1}(x_1)\,\mathbb{1}_{A_2}(x_2)$ is $\mathcal{E}_2$-measurable, and \begin{align*} \int_{E_2} \mathbb{1}_{A_1 \times A_2}(x_1, x_2)\,\mu_2(dx_2) = \mathbb{1}_{A_1}(x_1)\,\mu_2(A_2). \end{align*} The function $x_1 \mapsto \mathbb{1}_{A_1}(x_1)\,\mu_2(A_2)$ is $\mathcal{E}_1$-measurable, and integrating against $\mu_1$: \begin{align*} \int_{E_1}\!\left(\int_{E_2} \mathbb{1}_{A_1 \times A_2}(x_1, x_2)\,\mu_2(dx_2)\right)\mu_1(dx_1) = \mu_1(A_1)\,\mu_2(A_2) = \mu(A_1 \times A_2). \end{align*} The same computation with the order of integration reversed gives the identity for both iterated integrals. [/step] [step:Extend to all product-measurable sets via the Dynkin $\pi$-system lemma] [claim:Iterated Integral For All Measurable Sets] For every $C \in \mathcal{E}_1 \otimes \mathcal{E}_2$, the section $x_2 \mapsto \mathbb{1}_C(x_1, x_2)$ is $\mathcal{E}_2$-measurable for each $x_1$, the function $x_1 \mapsto \mu_2(C_{x_1})$ is $\mathcal{E}_1$-measurable, and \begin{align*} \mu(C) = \int_{E_1} \mu_2(C_{x_1})\,\mu_1(dx_1). \end{align*} [/claim] [proof] We first treat the case of finite measures, then extend to $\sigma$-finite. Assume $\mu_1(E_1) < \infty$ and $\mu_2(E_2) < \infty$. Define \begin{align*} \mathcal{D} = \left\{ C \in \mathcal{E}_1 \otimes \mathcal{E}_2 : \text{the three conclusions hold for } C \right\}. \end{align*} The previous step shows that $\mathcal{D}$ contains the $\pi$-system $\mathcal{R} = \{A_1 \times A_2 : A_1 \in \mathcal{E}_1,\, A_2 \in \mathcal{E}_2\}$ of measurable rectangles. We show $\mathcal{D}$ is a $d$-system. First, $E_1 \times E_2 \in \mathcal{D}$ (take $A_1 = E_1$, $A_2 = E_2$). Second, if $C, D \in \mathcal{D}$ with $C \subseteq D$, then $(D \setminus C)_{x_1} = D_{x_1} \setminus C_{x_1}$, so $x_2 \mapsto \mathbb{1}_{D \setminus C}(x_1, x_2)$ is measurable and $\mu_2((D \setminus C)_{x_1}) = \mu_2(D_{x_1}) - \mu_2(C_{x_1})$ (both finite since $\mu_2(E_2) < \infty$). The function $x_1 \mapsto \mu_2(D_{x_1}) - \mu_2(C_{x_1})$ is measurable, and \begin{align*} \int_{E_1} \mu_2((D \setminus C)_{x_1})\,\mu_1(dx_1) = \mu(D) - \mu(C) = \mu(D \setminus C). \end{align*} Third, if $(C_n)$ is increasing in $\mathcal{D}$ with $C = \bigcup_n C_n$, then $C_{x_1} = \bigcup_n (C_n)_{x_1}$ is measurable, $\mu_2(C_{x_1}) = \lim_n \mu_2((C_n)_{x_1})$ by continuity from below, and $x_1 \mapsto \mu_2(C_{x_1})$ is measurable as a pointwise limit. By the [Monotone Convergence Theorem](/theorems/509), \begin{align*} \int_{E_1} \mu_2(C_{x_1})\,\mu_1(dx_1) = \lim_n \int_{E_1} \mu_2((C_n)_{x_1})\,\mu_1(dx_1) = \lim_n \mu(C_n) = \mu(C). \end{align*} So $\mathcal{D}$ is a $d$-system containing the $\pi$-system $\mathcal{R}$. By the [Dynkin $\pi$-system lemma](/theorems/505), $\mathcal{E}_1 \otimes \mathcal{E}_2 = \sigma(\mathcal{R}) \subseteq \mathcal{D}$. For the $\sigma$-finite case: write $E_1 = \bigcup_j F_j$ and $E_2 = \bigcup_k G_k$ with $\mu_1(F_j) < \infty$ and $\mu_2(G_k) < \infty$. For any $C \in \mathcal{E}_1 \otimes \mathcal{E}_2$, the sets $C \cap (F_j \times G_k)$ increase to $C$ as $j, k \to \infty$. The finite-measure case applies to each $C \cap (F_j \times G_k)$, and the [Monotone Convergence Theorem](/theorems/509) extends the identity to $C$. [/proof] [/step] [step:Pass to non-negative measurable functions via simple-function approximation and MCT] [claim:Fubini For Non Negative Functions] For $f: E_1 \times E_2 \to [0, \infty]$ measurable, the section $x_2 \mapsto f(x_1, x_2)$ is $\mathcal{E}_2$-measurable for each $x_1$, the function \begin{align*} \varphi: E_1 &\to [0, \infty] \\ x_1 &\mapsto \int_{E_2} f(x_1, x_2)\,\mu_2(dx_2) \end{align*} is $\mathcal{E}_1$-measurable, and $\int_{E_1 \times E_2} f\,d\mu = \int_{E_1} \varphi\,d\mu_1$. [/claim] [proof] By linearity and the previous step, the identity holds for all non-negative simple functions on $\mathcal{E}_1 \otimes \mathcal{E}_2$. Choose non-negative simple functions $\phi_n \uparrow f$ pointwise (by the standard dyadic approximation). For each $n$, \begin{align*} \int_{E_1 \times E_2} \phi_n\,d\mu = \int_{E_1}\!\left(\int_{E_2} \phi_n(x_1, x_2)\,\mu_2(dx_2)\right)\mu_1(dx_1). \end{align*} For fixed $x_1$, $\phi_n(x_1, \cdot) \uparrow f(x_1, \cdot)$ pointwise on $E_2$. By the [Monotone Convergence Theorem](/theorems/509) applied to $\mu_2$, \begin{align*} \int_{E_2} \phi_n(x_1, x_2)\,\mu_2(dx_2) \uparrow \int_{E_2} f(x_1, x_2)\,\mu_2(dx_2) = \varphi(x_1). \end{align*} The functions $x_1 \mapsto \int_{E_2} \phi_n(x_1, \cdot)\,d\mu_2$ are measurable, so $\varphi$ is measurable as a pointwise limit. Applying the [Monotone Convergence Theorem](/theorems/509) to $\mu_1$: \begin{align*} \int_{E_1} \varphi\,d\mu_1 = \lim_n \int_{E_1}\!\left(\int_{E_2} \phi_n\,\mu_2(dx_2)\right)\mu_1(dx_1) = \lim_n \int_{E_1 \times E_2} \phi_n\,d\mu = \int_{E_1 \times E_2} f\,d\mu. \end{align*} [/proof] The identity with the order of integration reversed follows by the same argument with the roles of $(E_1, \mu_1)$ and $(E_2, \mu_2)$ exchanged. [/step] [step:Handle integrable functions by splitting $f = f^+ - f^-$] Let $f: E_1 \times E_2 \to \mathbb{R}$ be integrable. Write $f = f^+ - f^-$. By the previous step applied to $|f| = f^+ + f^-$, \begin{align*} \int_{E_1}\!\left(\int_{E_2} |f(x_1, x_2)|\,\mu_2(dx_2)\right)\mu_1(dx_1) = \int_{E_1 \times E_2} |f|\,d\mu < \infty. \end{align*} Since the outer integral is finite, the inner integral $\int_{E_2} |f(x_1, \cdot)|\,d\mu_2$ is finite for $\mu_1$-a.e. $x_1$, meaning $x_2 \mapsto f(x_1, x_2)$ is $\mu_2$-integrable for $\mu_1$-a.e. $x_1$. Applying the previous step to $f^+$ and $f^-$ separately and subtracting: \begin{align*} \int_{E_1 \times E_2} f\,d\mu &= \int_{E_1 \times E_2} f^+\,d\mu - \int_{E_1 \times E_2} f^-\,d\mu \\ &= \int_{E_1}\!\left(\int_{E_2} f^+\,\mu_2(dx_2)\right)\mu_1(dx_1) - \int_{E_1}\!\left(\int_{E_2} f^-\,\mu_2(dx_2)\right)\mu_1(dx_1) \\ &= \int_{E_1}\!\left(\int_{E_2} f(x_1, x_2)\,\mu_2(dx_2)\right)\mu_1(dx_1), \end{align*} where the last equality uses linearity of the inner integral (valid $\mu_1$-a.e. since both $\int f^+\,d\mu_2$ and $\int f^-\,d\mu_2$ are finite $\mu_1$-a.e.). [/step]