Theorem: Integral of Integrable Function is Additive

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f, g: X \to \R$ be $\mu$-integrable functions.
Then $f + g$ is $\mu$-integrable, with:
:$\ds \int \paren {f + g} \rd \mu = \int f \rd \mu + \int g \rd \mu$

Proof:
=== Lemma ===
{{:Integral of Integrable Function is Additive/Lemma}}{{qed|lemma}}
From Pointwise Sum of Measurable Functions is Measurable:
:$f + g$ is $\Sigma$-measurable.
From Function Measurable iff Positive and Negative Parts Measurable we have that: 
:$\paren {f + g}^+$ and $\paren {f + g}^-$ are $\Sigma$-measurable.
Since $f$ and $g$ are $\mu$-integrable, we have that $f$ and $g$ are also $\Sigma$-measurable.
Then from Function Measurable iff Positive and Negative Parts Measurable we have that:
:$f^+$, $f^-$, $g^+$ and $g^-$ are $\Sigma$-measurable.
We now want to show that: 
:$\ds \int \paren {f + g}^+ \rd \mu < \infty$
and:
:$\ds \int \paren {f + g}^- \rd \mu < \infty$
From Bound for Positive Part of Pointwise Sum of Functions, we have: 
:$\paren {f + g}^+ \le f^+ + g^+$
Then: 
{{begin-eqn}}
{{eqn | l = \int \paren {f + g}^+ \rd \mu
      | o = \le
      | r = \int \paren {f^+ + g^+} \rd \mu
}}
{{eqn | r = \int f^+ \rd \mu + \int g^+ \rd \mu
      | c = Integral of Positive Measurable Function is Additive
}}
{{eqn | o = <
      | r = \infty
      | c = since $f$ and $g$ are $\mu$-integrable, both integrals are finite
}}
{{end-eqn}}
From Bound for Negative Part of Pointwise Sum of Functions, we have: 
:$\paren {f + g}^- \le f^- + g^-$
Then: 
{{begin-eqn}}
{{eqn | l = \int \paren {f + g}^- \rd \mu
      | o = \le
      | r = \int \paren {f^- + g^-} \rd \mu
}}
{{eqn | r = \int f^- \rd \mu + \int g^- \rd \mu
      | c = Integral of Positive Measurable Function is Additive
}}
{{eqn | o = <
      | r = \infty
      | c = since $f$ and $g$ are $\mu$-integrable, both integrals are finite
}}
{{end-eqn}}
Now, we will show that: 
:$\ds \int \paren {f + g} \rd \mu = \int f \rd \mu + \int g \rd \mu$ 
From Difference of Positive and Negative Parts, we have: 
:$f + g = \paren {f + g}^+ - \paren {f + g}^-$
On the other hand, we have: 
{{begin-eqn}}
{{eqn | l = f + g
      | r = \paren {f^+ - f^-} + \paren {g^+ - g^-}
      | c = Difference of Positive and Negative Parts
}}
{{eqn | r = \paren {f^+ + g^+} - \paren {f^- + g^-}
}}
{{end-eqn}}
That is: 
:$\paren {f^+ + g^+} - \paren {f^- + g^-} = \paren {f + g}^+ - \paren {f + g}^-$
From Integral of Positive Measurable Function is Additive, we have: 
:$f^+ + g^+$ and $f^- + g^-$ are $\mu$-integrable.
From the {{Lemma|Integral of Integrable Function is Additive}}, we then have: 
:$\ds \int \paren {f^+ + g^+} \rd \mu - \int \paren {f^- + g^-} \rd \mu = \int \paren {f + g}^+ \rd \mu - \int \paren {f + g}^- \rd \mu$ 
From Integral of Positive Measurable Function is Additive, we have: 
:$\ds \int \paren {f^+ + g^+} \rd \mu = \int f^+ \rd \mu + \int g^+ \rd \mu$
and:
:$\ds \int \paren {f^- + g^-} \rd \mu = \int f^- \rd \mu + \int g^- \rd \mu$ 
Hence: 
{{begin-eqn}}
{{eqn | l = \int \paren {f + g} \rd \mu
      | r = \int \paren {f + g}^+ \rd \mu - \int \paren {f + g}^- \rd \mu
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{eqn | r = \int f^+ \rd \mu + \int g^+ \rd \mu - \paren {\int f^- \rd \mu + \int g^- \rd \mu}
}}
{{eqn | r = \paren {\int f^+ \rd \mu - \int f^- \rd \mu} + \paren {\int g^+ \rd \mu - \int g^- \rd \mu}
}}
{{eqn | r = \int f \rd \mu + \int g \rd \mu
      | c = {{Defof|Integral of Measure-Integrable Function}}
}}
{{end-eqn}}
{{qed}}