let a, b, c, d 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'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
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'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
assume A1: ( a <= b & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))

per cases ( not c <= d or c <= d ) ;

suppose A2: not c <= d ; :: thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))

['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then ( c <= b & a <= d ) by A1, XXREAL_1:1;
then A3: ['d,c'] c= dom f by A1, A2, INTEGR19:2;
integral (f,a,c) = (integral (f,a,d)) + (integral (f,d,c)) by A1, A2, Th1931;
then (integral (f,a,c)) - (integral (f,d,c)) = (integral (f,a,d)) + ((integral (f,d,c)) - (integral (f,d,c))) by RLVECT_1:28
.= (integral (f,a,d)) + (0. Y) by RLVECT_1:15 ;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A3, A2, Th1947; :: thesis: verum

end;

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

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

end;

end;