Proof of Linearity and Monotonicity of the Lebesgue Integral, and the Integrability Criterion

Conventions. Integrals of $f^{\pm}$ and of functions named as elements of $\mathcal{M}^{+}$ are taken in $\mathcal{M}^{+}$, integrals of elements of $\mathcal{L}^{1}(\mu)$ in $\mathcal{L}^{1}(\mu)$; where a function lies in both, the integral meant is named. For $f\in\mathcal{L}^{1}(\mu)$, $f$ is measurable, $f^{+},f^{-}\in\mathcal{M}^{+}$ have real integrals and $\int_{X}f\,d\mu=\int_{X}f^{+}\,d\mu-\int_{X}f^{-}\,d\mu$; a measurable $f:X\to\mathbb{R}$ with $\int_{X}f^{+}\,d\mu<\infty$ and $\int_{X}f^{-}\,d\mu<\infty$ lies in $\mathcal{L}^{1}(\mu)$ (Integrable Functions and Their Lebesgue Integral (i), Integrable Functions and Their Lebesgue Integral (ii), Integrable Functions and Their Lebesgue Integral (iii), Measurable Map, and the Set of Measurable Maps (ii)). Real numbers $\ge0$ lie in $[0,\infty]$, where their sums and products are the real ones (The Extended Real Line, Its Order, and [0,∞] (ii), Addition and Multiplication on [0,∞] (i), Addition and Multiplication on [0,∞] (ii)); an element of $[0,\infty]$ is a real number if and only if it is $<\infty$ (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)); and the order of $[-\infty,\infty]$ agrees with that of $\mathbb{R}$ on reals (Order and Suprema in the Extended Real Line (i)). Real arithmetic and order are those of the ordered field $\mathbb{R}$, read in the type $\mathrm{Real}$ (The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i), The Real Numbers as a Type (iv), The Real Numbers as a Type (v), The Real Numbers as a Type (vi), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i)).

Proof of (i): approximation. Let $f,g\in\mathcal{M}^{+}$, measurable into $[0,\infty]$ by Nonnegative Measurable Maps and Their Lebesgue Integral (i), and let $s_{m}=s_{m}(f)$ and $t_{m}=s_{m}(g)$ be their dyadic approximations. By Approximation of Measurable Functions by Dyadic Simple Functions (i), $s_{m},t_{m}\in\mathcal{S}^{+}$ and, for all $x\in X$ and $m\in\mathbb{N}$,

$$s_{m}(x)\le s_{m+1}(x),\qquad t_{m}(x)\le t_{m+1}(x),\qquad \sup_{m}s_{m}(x)=f(x),\qquad \sup_{m}t_{m}(x)=g(x).$$

Let $\varphi_{m}=s_{m}+t_{m}$, the sum of real-valued functions of Pointwise Operations on Real-Valued Maps (i); then $\varphi_{m}\in\mathcal{S}^{+}$ by Properties of Simple Functions and of the Simple Integral (ii), and $s_{m},t_{m},\varphi_{m}\in\mathcal{M}^{+}$ with $\int_{X}s_{m}\,d\mu=I_{\mu}(s_{m})$, $\int_{X}t_{m}\,d\mu=I_{\mu}(t_{m})$ and $\int_{X}\varphi_{m}\,d\mu=I_{\mu}(\varphi_{m})$ by Basic Properties of the Integral of Nonnegative Measurable Maps (i) (the sequences $(\varphi_{m})$, $(I_{\mu}(s_{m}))$, $(I_{\mu}(t_{m}))$ and $(\int_{X}\varphi_{m}\,d\mu)$ exist by Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iv) and Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii)).

Proof of (i): pointwise suprema. Let $x\in X$. The sequences $(s_{m}(x))_{m}$ and $(t_{m}(x))_{m}$ in $[0,\infty]$ are nondecreasing, and $\varphi_{m}(x)=s_{m}(x)+t_{m}(x)\le s_{m+1}(x)+t_{m+1}(x)=\varphi_{m+1}(x)$, so

$$\sup_{m}\varphi_{m}(x)=\sup_{m}s_{m}(x)+\sup_{m}t_{m}(x)=f(x)+g(x)=(f+g)(x)$$

(Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (i), Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (iv), Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i), Suprema and Finite Sums in [0,∞] (iii), Sums, Multiples and Products of Functions into [0,∞] (i)).

Proof of (i): monotone convergence. By Monotone Convergence Theorem (i) and Monotone Convergence Theorem (ii), applied to $(\varphi_{m})$ and $f+g$, to $(s_{m})$ and $f$, and to $(t_{m})$ and $g$, we get $f+g\in\mathcal{M}^{+}$ and the suprema of integrals below. As $I_{\mu}(\varphi_{m})=I_{\mu}(s_{m})+I_{\mu}(t_{m})$ by Properties of Simple Functions and of the Simple Integral (iv), and $(I_{\mu}(s_{m}))_{m}$ and $(I_{\mu}(t_{m}))_{m}$ are nondecreasing by Properties of Simple Functions and of the Simple Integral (vi), Suprema and Finite Sums in [0,∞] (iii) gives

$$\int_{X}(f+g)\,d\mu=\sup_{m}\bigl(I_{\mu}(s_{m})+I_{\mu}(t_{m})\bigr)=\sup_{m}I_{\mu}(s_{m})+\sup_{m}I_{\mu}(t_{m})=\int_{X}f\,d\mu+\int_{X}g\,d\mu .$$

Proof of (ii): induction. Let $(f_{k})$ be a sequence in $\mathcal{M}^{+}$, so that each $f_{k}$ is a function $X\to[0,\infty]$ (Nonnegative Measurable Maps and Their Lebesgue Integral (i)), and let $c_{k}=\int_{X}f_{k}\,d\mu$, the sequence $(c_{k})$ in $[0,\infty]$ existing by Maps and Relations Given by Formulas (i). By Partial Sums of a Sequence of Functions into [0,∞] (i) there is a sequence $(H_{n})$ of functions $X\to[0,\infty]$ with

$$H_{n}(x)=\sum_{k=1}^{n}f_{k}(x)\qquad(n\in\mathbb{N},\ x\in X),$$

the $n$-th partial sum of $(f_{k}(x))_{k}$. For $x\in X$ and $n\in\mathbb{N}$, Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums (i) and Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums (ii), applied to $(f_{k}(x))_{k}$ (a sequence by Evaluating a Sequence of Maps at a Point Gives a Sequence, and Its Range (i)), and Sums, Multiples and Products of Functions into [0,∞] (i) give

$$H_{1}(x)=f_{1}(x),\qquad H_{n+1}(x)=H_{n}(x)+f_{n+1}(x)=(H_{n}+f_{n+1})(x),$$

so $H_{1}=f_{1}$ and $H_{n+1}=H_{n}+f_{n+1}$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i)). We show by induction (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)) that $H_{n}\in\mathcal{M}^{+}$ and $\int_{X}H_{n}\,d\mu=\sum_{k=1}^{n}c_{k}$ for every $n\in\mathbb{N}$. For $n=1$, $H_{1}=f_{1}\in\mathcal{M}^{+}$ and $\int_{X}H_{1}\,d\mu=c_{1}=\sum_{k=1}^{1}c_{k}$ (Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums (i), applied to $(c_{k})$). If the claim holds for $n$, then $H_{n+1}=H_{n}+f_{n+1}$ with $H_{n},f_{n+1}\in\mathcal{M}^{+}$, so by (i) $H_{n+1}\in\mathcal{M}^{+}$ and

$$\int_{X}H_{n+1}\,d\mu=\int_{X}H_{n}\,d\mu+c_{n+1}=\sum_{k=1}^{n}c_{k}+c_{n+1}=\sum_{k=1}^{n+1}c_{k}$$

(Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums (ii), applied to $(c_{k})$).

Proof of (ii): passage to the limit. Let $x\in X$. As $H_{n}(x)$ is the $n$-th partial sum of $(f_{k}(x))_{k}$, Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (i) gives $H_{n}(x)\le H_{n+1}(x)$ for every $n\in\mathbb{N}$, and Sum of a Sequence in [0,∞] (ii) gives

$$\sup_{n}H_{n}(x)=\sum_{k\in\mathbb{N}}f_{k}(x)=\Bigl(\sum_{k}f_{k}\Bigr)(x).$$

So $(H_{n})$ is a sequence in $\mathcal{M}^{+}$, nondecreasing at every point, with pointwise supremum $\sum_{k}f_{k}$, and Monotone Convergence Theorem (i) and Monotone Convergence Theorem (ii), applied to $(H_{n})$ and $\sum_{k}f_{k}$, give $\sum_{k}f_{k}\in\mathcal{M}^{+}$ and

$$\int_{X}\sum_{k}f_{k}\,d\mu=\sup_{n}\int_{X}H_{n}\,d\mu=\sup_{n}\sum_{k=1}^{n}c_{k}=\sum_{k\in\mathbb{N}}c_{k},$$

the second equality by the induction, the last by Sum of a Sequence in [0,∞] (ii) applied to $(c_{k})$.

Proof of (iii). Let $f:X\to\mathbb{R}$ and $x\in X$; then $f^{+}(x)=\max\{f(x),0\}$ and $f^{-}(x)=\max\{-f(x),0\}$ (Positive Part, Negative Part and Absolute Value of a Real-Valued Function (i), Positive Part, Negative Part and Absolute Value of a Real-Valued Function (ii)). If $f(x)\ge0$, then $-f(x)\le0$, so $f^{+}(x)=f(x)$ and $f^{-}(x)=0$; if $f(x)\le0$, then $0\le-f(x)$, so $f^{+}(x)=0$ and $f^{-}(x)=-f(x)$ (Rules of Arithmetic and Order in an Ordered Field (v), The Maximum and Minimum of Two Elements of a Total Order (ii)). This is the last sentence. As $f(x)\ge0$ or $f(x)<0$ (Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders (vii)), and $|f(x)|=f(x)$ in the first case and $|f(x)|=-f(x)$ in the second (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii)),

$$f^{+}(x)-f^{-}(x)=f(x),\qquad f^{+}(x)+f^{-}(x)=|f(x)|$$

in both cases ($f(x)-0=f(x)$, $0-(-f(x))=f(x)$, $f(x)+0=f(x)$ and $0+(-f(x))=-f(x)$, by The Real Numbers as a Type (iv) and Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i)). These are the values at $x$ of $f^{+}-f^{-}$ and $f^{+}+f^{-}$ and of $f$ and $|f|$ (Pointwise Operations on Real-Valued Maps (i), Positive Part, Negative Part and Absolute Value of a Real-Valued Function (iii)), so $f=f^{+}-f^{-}$ and $|f|=f^{+}+f^{-}$.

Proof of (iv). Let $f:X\to\mathbb{R}$ be measurable. Then $|f|$ is measurable into $\mathbb{R}$ (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i), Measurable Map, and the Set of Measurable Maps (ii)), with values $\ge0$, hence measurable into $[0,\infty]$ (Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vii)), and $|f|\in\mathcal{M}^{+}$ (Nonnegative Measurable Maps and Their Lebesgue Integral (i)); also $f^{+},f^{-}\in\mathcal{M}^{+}$ (Integrable Functions and Their Lebesgue Integral (i)). By (iii), $|f|=f^{+}+f^{-}$, which is also the sum of $f^{+},f^{-}\in\mathcal{M}^{+}$ as functions into $[0,\infty]$ (Sums, Multiples and Products of Functions into [0,∞] (i)); so (i) gives the first display of (iv),

$$\int_{X}|f|\,d\mu=\int_{X}f^{+}\,d\mu+\int_{X}f^{-}\,d\mu .$$

If $f\in\mathcal{L}^{1}(\mu)$, the right-hand side is a sum of reals, so $\int_{X}|f|\,d\mu<\infty$. Conversely, if $\int_{X}|f|\,d\mu<\infty$, then $\int_{X}f^{\pm}\,d\mu\le\int_{X}|f|\,d\mu$ gives $\int_{X}f^{\pm}\,d\mu<\infty$ (Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (v), Arithmetic in [0,∞]: Monoid Laws, Distributivity, Monotonicity and Cancellation (i), Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii)), and $f\in\mathcal{L}^{1}(\mu)$.

Proof of (vi). Let $f:X\to\mathbb{R}$ be measurable with $f(x)\ge0$ for every $x$. Then $f$ is measurable into $[0,\infty]$, so $f\in\mathcal{M}^{+}$ (Measurable Maps: Generators, Composition, Continuous Maps, Restrictions, and Criteria for Real- and [0,∞]-Valued Maps (vii), Nonnegative Measurable Maps and Their Lebesgue Integral (i)). By (iii), $f^{+}=f$ and $f^{-}$ is the zero function, so $\int_{X}f^{-}\,d\mu=0<\infty$ (Basic Properties of the Integral of Nonnegative Measurable Maps (v)). Hence $f\in\mathcal{L}^{1}(\mu)$ if and only if $\int_{X}f\,d\mu=\int_{X}f^{+}\,d\mu<\infty$, the integral in $\mathcal{M}^{+}$; and then this integral is a real number (Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (ii)) and

$$\int_{X}f\,d\mu\;(\text{in }\mathcal{L}^{1}(\mu))=\int_{X}f^{+}\,d\mu-\int_{X}f^{-}\,d\mu=\int_{X}f^{+}\,d\mu-0=\int_{X}f\,d\mu\;(\text{in }\mathcal{M}^{+}).$$

Proof of (v). Let $f$ and $g$ be as there. As $g\in\mathcal{L}^{1}(\mu)$ is measurable and $g(x)\ge|f(x)|\ge0$ (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii)), (vi) gives $g\in\mathcal{M}^{+}$ with $\int_{X}g\,d\mu<\infty$ in $\mathcal{M}^{+}$. By (iv), $|f|\in\mathcal{M}^{+}$; as $|f|(x)\le g(x)$ for every $x$,

$$\int_{X}|f|\,d\mu\le\int_{X}g\,d\mu<\infty$$

(Basic Properties of the Integral of Nonnegative Measurable Maps (iii), Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii)), and $f\in\mathcal{L}^{1}(\mu)$ by (iv).

Proof of (vii): a rule for the maximum. Let $d,y\in\mathbb{R}$ with $d\ge0$; then $\max\{dy,0\}=d\max\{y,0\}$. If $d=0$, both sides are $0$. If $d>0$, then $0\le dy$ if and only if $0\le y$, and $dy\le0$ if and only if $y\le0$; so both sides equal $dy$ if $y\ge0$ and $0$ if $y\le0$ (Rules of Arithmetic and Order in an Ordered Field (i), Rules of Arithmetic and Order in an Ordered Field (vi), The Maximum and Minimum of Two Elements of a Total Order (ii)).

Proof of (vii): scalar multiples. Let $f\in\mathcal{L}^{1}(\mu)$ and $c\in\mathbb{R}$; we show $cf\in\mathcal{L}^{1}(\mu)$ and $\int_{X}cf\,d\mu=c\int_{X}f\,d\mu$. The function $cf$ is measurable (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i)). Let $p=\int_{X}f^{+}\,d\mu$ and $q=\int_{X}f^{-}\,d\mu$, reals $\ge0$. If $c\ge0$, the rule for the maximum and $-(cf(x))=c(-f(x))$ (Rules of Arithmetic and Order in an Ordered Field (ii)) give, for every $x\in X$,

$$(cf)^{+}(x)=\max\{cf(x),0\}=cf^{+}(x),\qquad (cf)^{-}(x)=\max\{c(-f(x)),0\}=cf^{-}(x),$$

so $(cf)^{\pm}=cf^{\pm}$ as functions into $[0,\infty]$ (Sums, Multiples and Products of Functions into [0,∞] (ii)), and Basic Properties of the Integral of Nonnegative Measurable Maps (iv) gives $\int_{X}(cf)^{+}\,d\mu=cp$ and $\int_{X}(cf)^{-}\,d\mu=cq$, both real. Hence $cf\in\mathcal{L}^{1}(\mu)$ and $\int_{X}cf\,d\mu=cp-cq=c(p-q)=c\int_{X}f\,d\mu$. If $c<0$, let $d=-c>0$ (Rules of Arithmetic and Order in an Ordered Field (v)); then $cf(x)=d(-f(x))$ and $-(cf(x))=df(x)$, so likewise $(cf)^{+}=df^{-}$, $(cf)^{-}=df^{+}$, and

$$\int_{X}cf\,d\mu=dq-dp=c(p-q)=c\int_{X}f\,d\mu$$

(Rules of Arithmetic and Order in an Ordered Field (ii), The Real Numbers as a Type (iv)).

Proof of (vii): sums are integrable. Let $f,g\in\mathcal{L}^{1}(\mu)$ and $w=f+g$, a measurable function (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i)). For $x\in X$, $f(x)\le f^{+}(x)$, $-f(x)\le f^{-}(x)$ and likewise for $g$, so $w(x)\le f^{+}(x)+g^{+}(x)$ and $-w(x)\le f^{-}(x)+g^{-}(x)$, and as the right-hand sides are $\ge0$,

$$w^{+}(x)\le f^{+}(x)+g^{+}(x),\qquad w^{-}(x)\le f^{-}(x)+g^{-}(x)$$

(The Maximum and Minimum of Two Elements of a Total Order (iii), The Maximum and Minimum of Two Elements of a Total Order (iv), Rules of Arithmetic and Order in an Ordered Field (iv), Rules of Arithmetic and Order in an Ordered Field (ii)). By (i), $f^{+}+g^{+}$ and $f^{-}+g^{-}$, formed in $[0,\infty]$, lie in $\mathcal{M}^{+}$ with integrals $\int_{X}f^{+}\,d\mu+\int_{X}g^{+}\,d\mu$ and $\int_{X}f^{-}\,d\mu+\int_{X}g^{-}\,d\mu$, which are real. By Basic Properties of the Integral of Nonnegative Measurable Maps (iii) and Small Facts about [0,∞]: Zero, Finiteness and Sums of Zeros (iii), $\int_{X}w^{+}\,d\mu<\infty$ and $\int_{X}w^{-}\,d\mu<\infty$, so $w\in\mathcal{L}^{1}(\mu)$.

Proof of (vii): the integral of a sum. By (iii), applied to $w$, $f$ and $g$, $w^{+}(x)-w^{-}(x)=f^{+}(x)-f^{-}(x)+g^{+}(x)-g^{-}(x)$ for every $x$, so, rearranging in $\mathbb{R}$, the functions into $[0,\infty]$ formed by sums in $[0,\infty]$ satisfy

$$(w^{+}+f^{-})+g^{-}=(w^{-}+f^{+})+g^{+}$$

(Sums, Multiples and Products of Functions into [0,∞] (i), The Real Numbers as a Type (iv)). Applying (i) twice on each side,

$$\Bigl(\int_{X}w^{+}\,d\mu+\int_{X}f^{-}\,d\mu\Bigr)+\int_{X}g^{-}\,d\mu=\Bigl(\int_{X}w^{-}\,d\mu+\int_{X}f^{+}\,d\mu\Bigr)+\int_{X}g^{+}\,d\mu .$$

All six integrals are real, so this is an identity in $\mathbb{R}$, and rearranging it gives $\int_{X}w\,d\mu=\int_{X}f\,d\mu+\int_{X}g\,d\mu$ (The Real Numbers as a Type (iv), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i)).

Proof of (vii): conclusion. Let $f,g\in\mathcal{L}^{1}(\mu)$ and $a,b\in\mathbb{R}$. By the step on scalar multiples, $af,bg\in\mathcal{L}^{1}(\mu)$ with integrals $a\int_{X}f\,d\mu$ and $b\int_{X}g\,d\mu$; by the two steps on sums, applied to $af$ and $bg$,

$$af+bg\in\mathcal{L}^{1}(\mu),\qquad \int_{X}(af+bg)\,d\mu=\int_{X}af\,d\mu+\int_{X}bg\,d\mu=a\int_{X}f\,d\mu+b\int_{X}g\,d\mu .$$

Proof of (viii): induction. Let $N$, $c$, $\Phi$ and $f_{j}$ be as there. For $l\in\mathbb{N}$ let $\psi(l)$ be the claim: if $l\in[N]$, the function $h_{l}:X\to\mathbb{R}$ with $h_{l}(x)=\sum_{j=1}^{l}c_{j}\Phi(j,x)$ lies in $\mathcal{L}^{1}(\mu)$ and $\int_{X}h_{l}\,d\mu=\sum_{j=1}^{l}c_{j}\int_{X}f_{j}\,d\mu$. For $x\in X$, the function $\Phi(\cdot,x):[N]\to\mathbb{R}$, $j\mapsto\Phi(j,x)$, is the composite of $\Phi$ with the function $[N]\to[N]\times X$, $j\mapsto(j,x)$, which pairs the identity of $[N]$ with the constant function with value $x$, and $j\mapsto c_{j}\Phi(j,x)$ is the function $[N]\to\mathbb{R}$ combining $c$ and $\Phi(\cdot,x)$ by the multiplication of $\mathbb{R}$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (iii), Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (i), Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (ii), Maps Formed Pointwise: Constant Maps, Pairs of Values, Maps Applied to Values, and Families of Maps (iii)); the functions $j\mapsto c_{j}\int_{X}f_{j}\,d\mu$ on $[N]$ and, for $l\in[N]$, $h_{l}$ on $X$ exist by Maps and Relations Given by Formulas (i). Here $[N]$ is finite and, for $l\in[N]$, $[l]\subseteq[N]$, so the sums over $[l]$ are those of the restrictions to $[l]$ of $j\mapsto c_{j}\Phi(j,x)$ and $j\mapsto c_{j}\int_{X}f_{j}\,d\mu$ (Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vii), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (v), Iterated Operations: Finite Sums and Finite Products (ii)). For $l=1$: $h_{1}(x)=c_{1}\Phi(1,x)$ (Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i)), so $h_{1}=c_{1}f_{1}+0f_{1}$, and (vii) gives $h_{1}\in\mathcal{L}^{1}(\mu)$ with $\int_{X}h_{1}\,d\mu=c_{1}\int_{X}f_{1}\,d\mu+0=\sum_{j=1}^{1}c_{j}\int_{X}f_{j}\,d\mu$ (The Real Numbers as a Type (iv)).

Proof of (viii): the inductive step. Let $\psi(l)$ hold and $l+1\in[N]$. Then $l\in[N]$ (Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (ii), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (v), Arithmetic and Order of the Natural Numbers (vi)), and $h_{l+1}=1h_{l}+c_{l+1}f_{l+1}$ by Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i). By $\psi(l)$ and (vii), $h_{l+1}\in\mathcal{L}^{1}(\mu)$ and

$$\int_{X}h_{l+1}\,d\mu=\int_{X}h_{l}\,d\mu+c_{l+1}\int_{X}f_{l+1}\,d\mu=\sum_{j=1}^{l}c_{j}\int_{X}f_{j}\,d\mu+c_{l+1}\int_{X}f_{l+1}\,d\mu=\sum_{j=1}^{l+1}c_{j}\int_{X}f_{j}\,d\mu$$

(Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i)). So $\psi(l)$ holds for every $l\in\mathbb{N}$ (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)); as $N\in[N]$ (Arithmetic and Order of the Natural Numbers (vi), Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i)) and $h_{N}=\sum_{j=1}^{N}c_{j}f_{j}$, $\psi(N)$ is the claim.

Proof of (ix). Let $f,g\in\mathcal{L}^{1}(\mu)$ with $f\le g$ pointwise. By (vii), $g-f=1g+(-1)f\in\mathcal{L}^{1}(\mu)$ with $\int_{X}(g-f)\,d\mu=\int_{X}g\,d\mu-\int_{X}f\,d\mu$. As $g-f$ is measurable and $(g-f)(x)=g(x)-f(x)\ge0$ for every $x$ (Rules of Arithmetic and Order in an Ordered Field (iv)), (vi) shows that this integral equals the integral of $g-f$ in $\mathcal{M}^{+}$, a real element of $[0,\infty]$ and so $\ge0$ (Order and Suprema in the Extended Real Line (viii)). Hence

$$\int_{X}g\,d\mu-\int_{X}f\,d\mu\ge0,\qquad\text{that is,}\qquad\int_{X}f\,d\mu\le\int_{X}g\,d\mu$$

(Rules of Arithmetic and Order in an Ordered Field (iv)).

Proof of (x). Let $f\in\mathcal{L}^{1}(\mu)$. By (iv), $|f|\in\mathcal{M}^{+}$ with finite integral in $\mathcal{M}^{+}$; as $|f|$ is measurable into $\mathbb{R}$ with values $\ge0$ (Arithmetic of Measurable Real- and [0,∞]-Valued Maps (i)), (vi) gives $|f|\in\mathcal{L}^{1}(\mu)$, with the same integral in both senses. By (iv), this integral is $p+q$, where $p=\int_{X}f^{+}\,d\mu$ and $q=\int_{X}f^{-}\,d\mu$ are reals $\ge0$. Since $\int_{X}f\,d\mu=p-q$,

$$\Bigl|\int_{X}f\,d\mu\Bigr|=|p+(-q)|\le|p|+|-q|=p+q=\int_{X}|f|\,d\mu$$

(Rules of Arithmetic and Order in an Ordered Field (xi), Rules of Arithmetic and Order in an Ordered Field (x), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i)).