let a, b, c be Real; :: thesis: 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; :: thesis: 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; :: thesis: ( 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'] ) ; :: thesis: ( 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose b <> c ; :: thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))

hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A1, Lm62; :: thesis: verum

end;

end;