let a, b, c be Real; for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
let Y be RealBanachSpace; for f being continuous PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f & c in ['a,b'] holds
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
let f be continuous PartFunc of REAL, the carrier of Y; ( a <= b & ['a,b'] c= dom f & c in ['a,b'] implies ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) )
assume A1:
( a <= b & ['a,b'] c= dom f & c in ['a,b'] )
; ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
then
['a,b'] = [.a,b.]
by INTEGRA5:def 3;
then A3:
( a <= c & c <= b )
by A1, XXREAL_1:1;
hence
( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] )
by A1, Th1909; integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
['c,b'] c= ['a,b']
by A3, INTEGR19:1;
then A5:
['c,b'] c= dom f
by A1;
per cases
( b = c or b <> c )
;
suppose A6:
b = c
;
integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))then A7:
['c,b'] = [.c,b.]
by INTEGRA5:def 3;
then A91:
integral (
f,
c,
b)
= integral (
f,
['c,b'])
by INTEGR18:16;
['c,b'] = [.(lower_bound ['c,b']),(upper_bound ['c,b']).]
by INTEGRA1:4;
then
(
lower_bound ['c,b'] = c &
upper_bound ['c,b'] = b )
by A7, INTEGRA1:5;
then
vol ['c,b'] = 0
by A6;
then
integral (
f,
c,
b)
= 0. Y
by A5, A91, INTEGR18:17;
hence
integral (
f,
a,
b)
= (integral (f,a,c)) + (integral (f,c,b))
by A6;
verum end;