Theorem: Sum of Integrals on Adjacent Intervals for Integrable Functions

Let $f$ be a real function which is Darboux integrable on any closed interval $\mathbb I$.
Let $a, b, c \in \mathbb I$.
Then:
:$\ds \int_a^c \map f t \rd t + \int_c^b \map f t \rd t = \int_a^b \map f t \rd t$

Proof:
=== Lemma ===
{{:Sum of Integrals on Adjacent Intervals for Integrable Functions/Lemma}}{{qed|lemma}}
{{WLOG}}, assume $a < b$.
First let $a < c < b$.
Let $P_1$ and $P_2$ be any subdivisions of $\closedint a c$ and $\closedint c b$ respectively.
Then $P = P_1 \cup P_2$ is a subdivision of $\closedint a b$.
From the definitions of upper Darboux sum and lower Darboux sum:
:$\map L {P_1} + \map L {P_2} = \map L P$
:$\map U {P_1} + \map U {P_2} = \map U P$
We consider the lower Darboux sum.
The same conclusion can be obtained by investigating the upper Darboux sum.
By definition of Darboux integral:
:$\ds \map L P \le \int_a^b \map f t \rd t$
Thus, given the subdivisions $P_1$ and $P_2$, we have:
:$\ds \map L {P_1} + \map L {P_2} \le \int_a^b \map f t \rd t$
and so:
:$\ds \map L {P_1} \le \int_a^b \map f t \rd t - \map L {P_2}$
So, for any subdivision $P_2$ of $\closedint c b$, $\ds \int_a^b \map f t \rd t - \map L {P_2}$ is an upper bound of $\map L {P_1}$.
Thus:
:$\ds \map {\sup_{P_1} } {\map L {P_1} } \le \int_a^b \map f t \rd t - \map L {P_2}$
where $\map {\sup_{P_1} } {\map L {P_1} }$ ranges over all subdivisions of $P_1$.
Thus by definition of definite integral:
:$\ds \int_a^c \map f t \rd t \le \int_a^b \map f t \rd t - \map L {P_2}$
and so:
:$\ds \map L {P_2} \le \int_a^b \map f t \rd t - \int_a^c \map f t \rd t$
Similarly, we find that:
:$\ds \int_c^b \map f t \rd t \le \int_a^b \map f t \rd t - \int_a^c \map f t \rd t$
Therefore:
:$\ds \int_a^b \map f t \rd t \ge \int_a^c \map f t \rd t + \int_c^b \map f t \rd t$
Having established the above, we now need to put it into context.
Let $P$ be ''any'' subdivision of $\closedint a b$, which may or may not include the point $c$.
Let $Q = P \cup \set c$ be the subdivision of $\closedint a b$ obtained from $P$ by including with it, if necessary, the point $c$.
We have $\map L P \le \map L Q$ by the lemma.
Let $Q_1$ be the subdivision of $\closedint a b$ which includes only the points of $Q$ that lie in $\closedint a c$.
Let $Q_2$ be the subdivision of $\closedint a b$ which includes only the points of $Q$ that lie in $\closedint c b$.
From the definition of lower Darboux sum:
:$\map L Q = \map L {Q_1} + \map L {Q_2}$
We have:
{{begin-eqn}}
{{eqn | l = \map L P
      | o = \le
      | r = \map L Q
      | c = 
}}
{{eqn | r = \map L {Q_1} + \map L {Q_2}
      | c = 
}}
{{eqn | o = \le
      | r = \int_a^c \map f t \rd t + \int_c^b \map f t \rd t
      | c = 
}}
{{end-eqn}}
So $\ds \int_a^c \map f t \rd t + \int_c^b \map f t \rd t$ is an upper bound for $\map L P$, where $P$ is any subdivision of $\closedint a b$.
Thus:
:$\ds \map {\sup_P} {\map L P} \le \int_a^c \map f t \rd t + \int_c^b \map f t \rd t$
Thus, by definition:
:$\ds \int_a^b \map f t \rd t \le \int_a^c \map f t \rd t + \int_c^b \map f t \rd t$
Combining this with the result:
:$\ds \int_a^b \map f t \rd t \ge \int_a^c \map f t \rd t + \int_c^b \map f t \rd t$
the result follows.
{{qed|lemma}}
Now suppose $a < b < c$.
Then from the definition of Darboux integral:
:$\ds \int_c^b \map f t \rd t := -\int_b^c \map f t \rd t$
and it follows that:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f t \rd t
      | r = \int_a^c \map f t \rd t - \int_b^c \map f t \rd t 
      | c = main result
}}
{{eqn | r = \int_a^c \map f t \rd t + \int_c^b \map f t \rd t
      | c = 
}}
{{end-eqn}}
The case of $c < a < b$ is proved similarly.
Finally, suppose $a = c < b$.
Then:
{{begin-eqn}}
{{eqn | l = \int_a^b \map f t \rd t
      | r = 0 + \int_c^b \map f t \rd t + \int_a^c \map f t \rd t
      | c = as $a = c$
}}
{{eqn | r = \int_a^c \map f t \rd t + \int_c^b \map f t \rd t
      | c = Integral on Zero Interval, as $a = c$
}}
{{end-eqn}}
The case of $a < c = b$ is proved similarly.
Hence the result, from Proof by Cases.
{{qed}}