avewright/proofwiki-math huggingface dataset:
Theorem: Relation Isomorphism Preserves Equivalence Relations

Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be relational structures.
Let $\struct {S, \RR_1}$ and $\struct {T, \RR_2}$ be (relationally) isomorphic.
Then $\RR_1$ is an equivalence relation {{iff}} $\RR_2$ is also an equivalence relation.

Proof:
Let $\phi: S \to T$ be a relation isomorphism.
By Inverse of Relation Isomorphism is Relation Isomorphism it follows that $\phi^{-1}: T \to S$ is also a relation isomorphism.
{{WLOG}}, it thus is necessary to prove only that if $\RR_1$ is an equivalence relation then $\RR_2$ is an equivalence relation.
So, suppose $\RR_1$ is an equivalence relation.
By definition:
:$(1): \quad \RR_1$ is reflexive
:$(2): \quad \RR_1$ is symmetric
:$(3): \quad \RR_1$ is transitive.
It follows that:
:From Relation Isomorphism Preserves Reflexivity, $\RR_2$ is reflexive.
:From Relation Isomorphism Preserves Symmetry, $\RR_2$ is symmetric.
:From Relation Isomorphism Preserves Transitivity, $\RR_2$ is transitive.
So by definition $\RR_2$ is an equivalence relation.
Hence the result.
{{qed}}
Theorem: Pointwise Supremum of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space, and let $I$ be a countable set.
Let $\family {f_i}_{i \mathop \in I}$, $f_i: X \to \overline \R$ be an $I$-indexed collection of $\Sigma$-measurable functions.
Then the pointwise supremum $\ds \sup_{i \mathop \in I} f_i: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
Let $a \in \R$; for all $i \in I$, we have by Characterization of Measurable Functions that:
:$\set {f_i > a} \in \Sigma$
and as $\Sigma$ is a $\sigma$-algebra and $I$ is countable, also:
:$\ds \bigcup_{i \mathop \in I} \set {f_i > a} \in \Sigma$
We will now show that:
:$\ds \set {\sup_{i \mathop \in I} f_i > a} = \bigcup_{i \mathop \in I} \set {f_i > a}$
First, observe that for all $i \in I$:
:$\map {f_i} x \le \ds \sup_{i \mathop \in I} \map {f_i} x$
and hence:
:$\set {f_i > a} \subseteq \ds \set {\sup_{i \mathop \in I} f_i > a}$
From Union is Smallest Superset: Family of Sets:
:$\ds \bigcup_{i \mathop \in I} \set {f_i > a} \subseteq \set {\sup_{i \mathop \in I} f_i > a}$
Next, suppose that:
:$x \notin \ds \bigcup_{i \mathop \in I} \set {f_i > a}$
Then, by definition of union:
:$\forall i \in I: \map {f_i} x \le a$
which is to say that $a$ is an upper bound for the $\map {f_i} x$.
Hence, by definition of supremum, it follows that:
:$\ds \sup_{i \mathop \in I} \map {f_i} x \le a$
and therefore:
:$x \notin \ds \set {\sup_{i \mathop \in I} f_i > a}$
Thus, we have shown:
:$\ds \set {\sup_{i \mathop \in I} f_i > a} = \bigcup_{i \mathop \in I} \set {f_i > a} \in \Sigma$
{{explain|There must be a result covering this type of set equality}}
and by Characterization of Measurable Functions, it follows that $\ds \sup_{i \mathop \in I} f_i$ is measurable.
{{qed}}
Theorem: Pointwise Infimum of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $I$ be a countable set.
Let $\family {f_i}_{i \mathop \in I}$, $f_i: X \to \overline \R$ be an $I$-indexed family of $\Sigma$-measurable functions.
Then the pointwise infimum $\ds \inf_{i \mathop \in I} f_i: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
From Infimum as Supremum, we have the Equality of Mappings:
:$\ds \inf_{i \mathop \in I} f_i = -\paren {\sup_{i \mathop \in I} \paren {-f_i} }$
Now, from Negative of Measurable Function is Measurable and Pointwise Supremum of Measurable Functions is Measurable, it follows that:
:$\ds - \paren {\sup_{i \mathop \in I} \paren {-f_i} }$
is a measurable function.
Hence the result.
{{qed}}
Theorem: Pointwise Upper Limit of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\sequence {f_n}_{n \mathop \in \N}$, $f_n: X \to \overline \R$ be a sequence of $\Sigma$-measurable functions.
Then the pointwise upper limit $\ds \limsup_{n \mathop \to \infty} f_n: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
By definition of upper limit, we have:
:$\ds \limsup_{n \mathop \to \infty} f_n = \inf_{m \mathop \in \N} \sup_{n \mathop \ge m} f_n$
The result follows from combining:
:Pointwise Supremum of Measurable Functions is Measurable
:Pointwise Infimum of Measurable Functions is Measurable
{{qed}}
Theorem: Pointwise Lower Limit of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\sequence {f_n}_{n \mathop \in \N}$, $f_n: X \to \overline \R$ be a sequence of $\Sigma$-measurable functions.
Then the pointwise lower limit:
:$\ds \liminf_{n \mathop \to \infty} f_n: X \to \overline \R$
is also $\Sigma$-measurable.

Proof:
By definition of limit inferior, we have:
:$\ds \liminf_{n \mathop \to \infty} f_n = \sup_{m \mathop \in \N} \ \inf_{n \mathop \ge m} f_n$
The result follows from combining:
:Pointwise Infimum of Measurable Functions is Measurable
:Pointwise Supremum of Measurable Functions is Measurable
{{qed}}
Theorem: Pointwise Limit of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\sequence {f_n}_{n \mathop \in \N}$, $f_n: X \to \overline \R$ be a sequence of $\Sigma$-measurable functions.
Then the pointwise limit $\ds \lim_{n \mathop \to \infty} f_n: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
From Convergence of Limsup and Liminf, it follows that:
:$\ds \lim_{n \mathop \to \infty} f_n = \limsup_{n \mathop \to \infty} f_n$
We have Pointwise Upper Limit of Measurable Functions is Measurable.
Hence the result.
{{qed}}
Theorem: Pointwise Sum of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Assume that the pointwise sum $f + g: X \to \overline \R$ is well-defined.
Then $f + g$ is a $\Sigma$-measurable function.

Proof:
By Measurable Function is Pointwise Limit of Simple Functions, we find sequences $\sequence {f_n}_{n \mathop \in \N}, \sequence {g_n}_{n \mathop \in \N}$ such that:
:$\ds f = \lim_{n \mathop \to \infty} f_n$
:$\ds g = \lim_{n \mathop \to \infty} g_n$
where the limits are pointwise.
It follows that for all $x \in X$:
:$\map f x + \map g x = \ds \lim_{n \mathop \to \infty} \map {f_n} x + \map {g_n} x$
{{explain|There needs to be a bunch of results establishing such equalities of convergence in function spaces}}
so that we have the pointwise limit:
:$\ds f + g = \lim_{n \mathop \to \infty} f_n + g_n$
By Pointwise Sum of Simple Functions is Simple Function, $f + g$ is a pointwise limit of simple functions.
By Simple Function is Measurable, $f + g$ is a pointwise limit of measurable functions.
Hence $f + g$ is measurable, by Pointwise Limit of Measurable Functions is Measurable.
{{qed}}
Theorem: Pointwise Difference of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Assume that the pointwise difference $f - g: X \to \overline \R$ is well-defined.
Then $f - g$ is a $\Sigma$-measurable function.

Proof:
We have the apparent identity:
:$f - g = f + \paren {-g}$
By Negative of Measurable Function is Measurable, $-g$ is a measurable function.
Hence so is $f - g$, by Pointwise Sum of Measurable Functions is Measurable.
{{qed}}
Theorem: Pointwise Product of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Then the pointwise product $f \cdot g: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
By Measurable Function is Pointwise Limit of Simple Functions, we find sequences $\sequence {f_n}_{n \mathop \in \N}, \sequence {g_n}_{n \mathop \in \N}$ such that:
:$\ds f = \lim_{n \mathop \to \infty} f_n$
:$\ds g = \lim_{n \mathop \to \infty} g_n$
where the limits are pointwise.
It follows that for all $x \in X$:
:$\map f x \cdot \map g x = \ds \lim_{n \mathop \to \infty} \map {f_n} x \cdot \map {g_n} x$
{{explain|There needs to be a bunch of results establishing such equalities of convergence in function spaces}}
so that we have the pointwise limit:
:$\ds f \cdot g = \lim_{n \mathop \to \infty} f_n \cdot g_n$
By Pointwise Product of Simple Functions is Simple Function, $f \cdot g$ is a pointwise limit of simple functions.
By Simple Function is Measurable, $f \cdot g$ is a pointwise limit of measurable functions.
Hence $f \cdot g$ is measurable, by Pointwise Limit of Measurable Functions is Measurable.
{{qed}}
Theorem: Pointwise Maximum of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Then the pointwise maximum $\max \set {f, g}: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
For all $x \in X$ and $a \in \R$, we have by Max Operation Yields Supremum of Parameters that:
:$\max \set {\map f x, \map g x} \le a$
{{iff}} both $\map f x \le a$ and $\map g x \le a$.
That is, for all $a \in \R$:
:$\set {x \in X: \max \set {\map f x, \map g x} \le a} = \set {x \in X: \map f x \le a} \cap \set {x \in X: \map g x \le a}$
By Characterization of Measurable Functions: $(1) \implies (2)$, the two sets on the RHS are elements of $\Sigma$, i.e. measurable.
By Sigma-Algebra Closed under Intersection, it follows that:
:$\set {x \in X: \max \set {\map f x, \map g x} \le a} \in \Sigma$
Hence $\max \set {f, g}$ is measurable, by Characterization of Measurable Functions: $(2) \implies (1)$.
{{qed}}
Theorem: Pointwise Minimum of Measurable Functions is Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Then the pointwise minimum $\min \set {f, g}: X \to \overline \R$ is also $\Sigma$-measurable.

Proof:
For all $x \in X$ and $a \in \R$, we have by Min Operation Yields Infimum of Parameters that:
:$a \le \min \set {\map f x, \map g  x}$
{{iff}} both $a \le \map f x$ and $a \le \map g x$.
That is, for all $a \in \R$:
:$\set {x \in X: \min \set {\map f x, \map g x} \ge a} = \set {x \in X: \map f x \ge a} \cap \set {x \in X: \map g x \ge a}$
By Characterization of Measurable Functions: $(1) \implies (4)$, the two sets on the RHS are elements of $\Sigma$, that is, measurable.
By Sigma-Algebra Closed under Intersection:
:$\set {x \in X: \min \set {\map f x, \map g x} \ge a} \in \Sigma$
Hence $\min \set {f, g}$ is measurable, by Characterization of Measurable Functions: $(4) \implies (1)$.
{{qed}}
Theorem: Function Measurable iff Positive and Negative Parts Measurable

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f: X \to \overline \R$ be an extended real-valued function.
Let $f^+, f^-: X \to \overline \R$ be the positive and negative parts of $f$.
Then $f$ is $\Sigma$-measurable {{iff}} both $f^+$ and $f^-$ are $\Sigma$-measurable.

Proof:
=== Necessary Condition ===
Suppose $f$ is measurable.
By definition, its positive part $f^+$ equals the pointwise maximum:
:$f^+ = \max \set {f, 0}$
where $0$ denotes the zero function.
By Constant Function is Measurable, $0$ is a measurable function.
Thus, by Pointwise Maximum of Measurable Functions is Measurable, $f^+$ is measurable.
Subsequently, the negative part $f^-$ of $f$ is defined by means of a pointwise minimum:
:$f^- = - \min \set {f, 0}$
By Pointwise Maximum of Measurable Functions is Measurable and Negative of Measurable Function is Measurable, $f^-$ is measurable as well.
{{qed|lemma}}
Theorem: Measurable Functions Determine Measurable Sets

Let $\struct {X, \Sigma}$ be a measurable space.
Let $f, g: X \to \overline \R$ be $\Sigma$-measurable functions.
Then the following sets are measurable:
:$\set {f < g}$
:$\set {f \le g}$
:$\set {f = g}$
:$\set {f \ne g}$
where, for example, $\set {f < g}$ is short for $\set {x \in X: \map f x < \map g x}$.

Proof:
From Pointwise Difference of Measurable Functions is Measurable, $f - g: X \to \overline \R$ is $\Sigma$-measurable.
Now we have the following evident identities:
:$\set {f < g} = \set {f - g < 0}$
:$\set {f \ge g} = \set {f - g \le 0}$
:$\set {f = g} = \set {f - g = 0}$
:$\set {f \ne g} = \set {f - g \ne 0}$
Subsequently, using the preimage under $f - g$, the latter may respectively be expressed as:
:$\set {f - g < 0} = \paren {f - g}^{-1} \sqbrk {\openint {-\infty} 0}$
:$\set {f - g \ge 0} = \paren {f - g}^{-1} \sqbrk {\hointl {-\infty} 0}$
:$\set {f - g = 0} = \paren {f - g}^{-1} \sqbrk {\set 0}$
:$\set {f - g \ne 0} = \paren {f - g}^{-1} \sqbrk {\R \setminus \set 0}$
Now the sets:
:$\openint {-\infty} 0$
:$\hointl {-\infty} 0$
:$\set 0$
:$\R \setminus \set 0$
are all open or closed in the Euclidean topology.
Hence by definition of Borel $\sigma$-algebra, and by Closed Set Measurable in Borel Sigma-Algebra, they are $\map \BB \R$-measurable.
Since $f - g$ is $\Sigma$-measurable, it follows that:
:$\set {f < g}$
:$\set {f \le g}$
:$\set {f = g}$
:$\set {f \ne g}$
are all $\Sigma$-measurable sets.
{{qed}}
Theorem: Factorization Lemma/Extended Real-Valued Function

An extended real-valued function $g: X \to \overline \R$ is $\map \sigma f$-measurable {{iff}}:
:There exists a $\Sigma$-measurable mapping $\tilde g: Y \to \overline \R$ such that $g = \tilde g \circ f$
where:
:$\map \sigma f$ denotes the $\sigma$-algebra generated by $f$

Proof:
=== Necessary Condition ===
Let $g$ be a $\map \sigma f \, / \, \overline \BB$-measurable function.
We need to construct a measurable $\tilde g$ such that $g = \tilde g \circ f$.
Let us proceed in the following fashion:
:Establish the result for $g$ a characteristic function;
:Establish the result for $g$ a simple function;
:Establish the result for all $g$
So let $g = \chi_E$ be a characteristic function.
By Characteristic Function Measurable iff Set Measurable, it follows that $E$ is $\map \sigma f$-measurable.
Thus there exists some $A \in \Sigma$ such that $E = \map {f^{-1} } A$.
Again by Characteristic Function Measurable iff Set Measurable, we have $\chi_A: Y \to \overline \R$ is measurable.
It follows that $\chi_E = \chi_A \circ f$, and $\tilde g := \chi_A$ works.
Now let $g = \ds \sum_{i \mathop = 1}^n a_i \chi_{E_i}$ be a simple function.
Let $A_i$ be associated to $E_i$ as above. Then we have:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n a_i \chi_{E_i}
      | r = \sum_{i \mathop = 1}^n a_i \paren {\chi_{A_i} \circ f}
      | c = by the result for characteristic functions
}}
{{eqn | r = \paren {\sum_{i \mathop = 1}^n a_i \chi_{A_i} } \circ f
      | c = Composition of Mappings is Linear
}}
{{end-eqn}}
Now $\ds \sum_{i \mathop = 1}^n a_i \chi_{A_i}$ is a simple function, hence measurable by Simple Function is Measurable.
Therefore, it suffices as a choice for $\tilde g$.
Next, let $g \ge 0$ be a measurable function.
By Measurable Function is Pointwise Limit of Simple Functions, we find simple functions $g_j$ such that:
:$\ds \lim_{j \mathop \to \infty} g_j = g$
Applying the previous step to each $g_j$, we find a sequence of $\tilde g_j$ satisfying:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = g$
From Composition with Pointwise Limit it follows that we have, putting $\tilde g := \ds \lim_{j \mathop \to \infty} \tilde g_j$:
:$\ds \lim_{j \mathop \to \infty} \tilde g_j \circ f = \tilde g \circ f$
{{explain|Address why (if?!) $\tilde g$ is well defined}}
An application of Pointwise Limit of Measurable Functions is Measurable yields $\tilde g$ measurable.
Thus we have provided a suitable $\tilde g$ for every $g$, such that:
:$g = \tilde g \circ f$
as desired.
{{qed}}
Theorem: Piecewise Combination of Measurable Mappings is Measurable/Binary Case

Let $f, g: X \to X'$ be $\Sigma \, / \, \Sigma'$-measurable mappings.
Let $E \in \Sigma$ be a measurable set.
Define $h: X \to X'$ by:
:$<nowiki>\forall x \in X: \map h x := \begin{cases}
\map f x & : \text {if $x \in E$} \\
\map g x & : \text {if $x \notin E$}
\end{cases}</nowiki>$
Then $h$ is also a $\Sigma \, / \, \Sigma'$-measurable mapping.

Proof:
Let $E' \in \Sigma'$ be a $\Sigma'$-measurable set.
Then by definition of preimage:
:$\map {h^{-1} } {E'} = \set {x \in X: \map h x \in E'}$
Expanding the definition of $h$, this translates into:
:$\map {h^{-1} } {E'} = \set {x \in E: \map f x \in E'} \cup \set {x \in \relcomp X E: \map g x \in E'}$
where $\complement$ denotes set complement.
That is, we have:
:$\map {h^{-1} } {E'} = \paren {E \cap \map {f^{-1} } {E'} } \cup \paren {\relcomp X E \cap \map {g^{-1} } {E'} }$
All sets on the {{RHS}} are $\Sigma$-measurable.
By Sigma-Algebra Closed under Intersection and Sigma-Algebra Closed under Union, so is $\map {h^{-1} } {E'}$.
Since $E' \in \Sigma'$ was arbitrary, $h$ is a $\Sigma \, / \, \Sigma'$-measurable mapping.
{{qed}}
Theorem: Piecewise Combination of Measurable Mappings is Measurable/General Case

Let $\sequence {E_n}_{n \mathop \in \N} \in \Sigma, \ds \bigcup_{n \mathop \in \N} E_n = X$ be a countable cover of $X$ by $\Sigma$-measurable sets.
For each $n \in \N$, let $f_n: E_n \to X'$ be a $\Sigma_{E_n} \, / \, \Sigma'$-measurable mapping.
Here, $\Sigma_{E_n}$ is the trace $\sigma$-algebra of $E_n$ in $\Sigma$.
Suppose that for every $m, n \in \N$, $f_m$ and $f_n$ satisfy:
:$(1): \quad f_m \restriction_{E_m \cap E_n} = f_n \restriction_{E_m \cap E_n}$
that is, $f_m$ and $f_n$ coincide whenever both are defined; here $\restriction$ denotes restriction.
Define $f: X \to X'$ by:
:$\ds \forall n \in \N, x \in E_n: \map f x := \map {f_n} x$
Then $f$ is a $\Sigma \, / \, \Sigma'$-measurable mapping.

Proof:
First, note that $f$ is well-defined, since if $x \in E_n$ and $x \in E_m$, we have that:
:$\map {f_n} x = \map f x = \map {f_m} x$
by $(1)$, since $x \in E_n \cap E_m$.
Let $E' \in \Sigma'$.
Then by definition of preimage, $f^{-1} \sqbrk {E'} \subseteq X$, and hence:
{{begin-eqn}}
{{eqn | l = f^{-1} \sqbrk {E'}
      | r = X \cap h^{-1} \sqbrk {E'}
      | c = Intersection with Subset is Subset
}}
{{eqn | r = \paren {\bigcup_{n \mathop \in \N} E_n} \cap f^{-1} \sqbrk {E'}
}}
{{eqn | r = \bigcup_{n \mathop \in \N} \paren {E_n \cap f^{-1} \sqbrk {E'} }
      | c = Intersection Distributes over Union: General Result
}}
{{eqn | r = \bigcup_{n \mathop \in \N} {f_n}^{-1} \sqbrk {E'}
}}
{{end-eqn}}
The last step we derive as follows.
Whenever $x \in E_n$, we have by definition of $f$ that $\map f x = \map {f_n} x$.
Hence, $x \in E_n \cap f^{-1} \sqbrk {E'}$ implies $x \in {f_n}^{-1} \sqbrk {E'}$.
Conversely, if $x \in {f_n}^{-1} \sqbrk {E'}$, that is $\map {f_n} x \in E'$, then $x \in E_n$ since $E_n$ is the domain of $f_n$.
By definition of $f$ then also $\map f x = \map {f_n} x \in E'$.
Hence we have deduced that $E_n \cap f^{-1} \sqbrk {E'} = {f_n}^{-1} \sqbrk {E'}$.
Since all $f_n$ are $\Sigma_{E_n} \, / \, \Sigma'$-measurable, it follows that for all $n \in \N$:
:${f_n}^{-1} \sqbrk {E'} \in \Sigma$
By $\sigma$-algebra axiom $(3)$, it follows that:
:$f^{-1} \sqbrk {E'} = \ds \bigcup_{n \mathop \in \N} {f_n}^{-1} \sqbrk {E'} \in \Sigma$
Since $E' \in \Sigma'$ was arbitrary, it follows that $f$ is $\Sigma \, / \, \Sigma'$-measurable.
{{qed}}
Theorem: Function Simple iff Positive and Negative Parts Simple

Let $\left({X, \Sigma}\right)$ be a measurable space.
Let $g: X \to \overline{\R}$ be an extended real-valued function.
Then $g$ is a simple function {{iff}} its positive part $g^+$ and negative part $g^-$ are simple functions.

Proof:
=== Necessary Condition ===
Suppose $g$ is a simple function.
By Positive Part of Simple Function is Simple Function, so is $g^+$.
By Negative Part of Simple Function is Simple Function, so is $g^-$.
{{qed|lemma}}
Theorem: Integral of Positive Simple Function is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f: X \to \R, f \in \EE^+$ be a positive simple function.
Then the $\mu$-integral of $f$, $\map {I_\mu} f$, is well-defined.
That is, for any two standard representations for $f$, say:
:$\ds f = \sum_{i \mathop = 0}^n a_i \chi_{E_i} = \sum_{j \mathop = 0}^m b_j \chi_{F_j}$
it holds that:
:$\ds \sum_{i \mathop = 0}^n a_i \map \mu {E_i} = \sum_{j \mathop = 0}^m b_j \map \mu {F_j}$

Proof:
The sets $F_0, \ldots, F_m$ are pairwise disjoint, and:
:$X = \ds \bigcup_{j \mathop = 0}^m F_j$
From Characteristic Function of Disjoint Union, we have:
:$\chi_X = \ds \sum_{j \mathop = 0}^m \chi_{F_j}$
Remark that $\map {\chi_X} x = 1$ for all $x \in X$, so that we have:
{{begin-eqn}}
{{eqn | l = f
      | r = \sum_{i \mathop = 0}^n a_i \chi_{E_i} \cdot 1
}}
{{eqn | r = \sum_{i \mathop = 0}^n a_i \chi_{E_i} \paren {\sum_{j \mathop = 0}^m \chi_{F_j} }
}}
{{eqn | r = \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \chi_{E_i} \chi_{F_j}
}}
{{eqn | r = \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \chi_{E_i \cap F_j}
      | c = Characteristic Function of Intersection: Variant 1
}}
{{end-eqn}}
Repeating the argument with the $E_i$ and $F_j$ interchanged also yields:
:$f = \ds \sum_{j \mathop = 0}^m \sum_{i \mathop = 0}^n b_j \chi_{F_j \cap E_i}$
Now whenever $x \in E_i \cap F_j$, for some $i, j$, then since the $E_i$, $F_j$ are disjoint, we find:
:$x \in E_{i'} \cap F_{j'}$ implies $i = i'$ and $j = j'$
Thus, evaluating both expressions for $\map f x$ we find:
:$a_i = \map f x = b_j$
In conclusion, we have:
:$a_i = b_j$
if $E_i \cap F_j \ne \O$.
Furthermore, we have for all $i$ that:
:$\ds E_i = E_i \cap X = E_i \cap \paren {\bigcup_{j \mathop = 0}^m F_j} = \bigcup_{j \mathop = 0}^m \paren {E_i \cap F_j}$
by Intersection Distributes over Union: General Result.
Similarly, we obtain for all $j$:
:$\ds F_j = F_j \cap X = F_j \cap \paren {\bigcup_{i \mathop = 0}^n E_i} = \bigcup_{i \mathop = 0}^n \paren {F_j \cap E_i}$
With this knowledge, we compute:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 0}^n a_i \map \mu {E_i}
      | r = \sum_{i \mathop = 0}^n a_i \map \mu {\bigcup_{j \mathop = 0}^m \paren {E_i \cap F_j} }
}}
{{eqn | r = \sum_{i \mathop = 0}^n a_i \sum_{j \mathop = 0}^m \map \mu {E_i \cap F_j}
      | c = Measure is Finitely Additive Function
}}
{{eqn | r = \sum_{i \mathop = 0}^n \sum_{j \mathop = 0}^m a_i \map \mu {E_i \cap F_j}
      | c = Summation is Linear
}}
{{eqn | r = \sum_{j \mathop = 0}^m \sum_{i \mathop = 0}^n b_j \map \mu {E_i \cap F_j}
      | c = If $a_i \ne b_j$ then $E_i \cap F_j = \O$; $a_i \cdot 0 = b_j \cdot 0$
}}
{{eqn | r = \sum_{j \mathop = 0}^m b_j \sum_{i \mathop = 0}^n \map \mu {E_i \cap F_j}
      | c = Summation is Linear
}}
{{eqn | r = \sum_{j \mathop = 0}^m b_j \map \mu {\bigcup_{i \mathop = 0}^n \paren {E_i \cap F_j} }
      | c = Measure is Finitely Additive Function
}}
{{eqn | r = \sum_{j \mathop = 0}^m b_j \map \mu {F_j}
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Integral of Characteristic Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $E \in \Sigma$ be a measurable set, and let $\chi_E: X \to \R$ be its characteristic function.
Then $\map {I_\mu} {\chi_E} = \map \mu E$, where $\map {I_\mu} {\chi_E}$ is the $\mu$-integral of $\chi_E$.

Proof:
Let $a_1 = 1$ and $E_1 = E$.
As in the definition of standard representation, denote $a_0 = 0$ and $E_0 = X \setminus E_1$.
Then for $x \in X$, we have:
:$\map {\chi_E} x = 0 \cdot \map {\chi_{E_0} } x + 1 \cdot \map {\chi_{E_1} } x$
since $E_1 = E$.
Hence $\chi_E = a_0 \chi_{E_0} + a_1 \chi_{E_1}$ is a standard representation for $\chi_E$.
Thus, by definition of $\mu$-integral:
:$\ds \int \chi_E \rd \mu = a_0 \map \mu {E_0} + a_1 \map \mu {E_1} = \map \mu E$
as desired.
{{qed}}