let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st a <= b & b <= c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] holds
( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )
let a, b, c be Real; :: thesis: ( a <= b & b <= c & ['a,c'] c= dom f & f | ['a,b'] is bounded & f | ['b,c'] is bounded & f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] implies ( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) ) )
assume that
A1: ( a <= b & b <= c ) and
A2: ['a,c'] c= dom f and
A3: f | ['a,b'] is bounded and
A4: f | ['b,c'] is bounded and
A5: f is_integrable_on ['a,b'] and
A6: f is_integrable_on ['b,c'] ; :: thesis: ( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )
thus A7: f is_integrable_on ['a,c'] :: thesis: integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c))

proof

per cases ( a <> b or a = b ) ;

suppose A8: a <> b ; :: thesis: f is_integrable_on ['a,c']

per cases ( b <> c or b = c ) ;

suppose b <> c ; :: thesis: f is_integrable_on ['a,c']

then ( a < b & b < c ) by A1, A8, XXREAL_0:1;
hence f is_integrable_on ['a,c'] by A2, A3, A4, A5, A6, Lm1; :: thesis: verum

end;

suppose b = c ; :: thesis: f is_integrable_on ['a,c']

hence f is_integrable_on ['a,c'] by A5; :: thesis: verum

end;

end;

end;

suppose a = b ; :: thesis: f is_integrable_on ['a,c']

hence f is_integrable_on ['a,c'] by A6; :: thesis: verum

end;

end;

end;

A9: a <= c by A1, XXREAL_0:2;
A10: ['a,c'] = [.a,c.] by A1, XXREAL_0:2, INTEGRA5:def 3;
then A11: b in ['a,c'] by A1, XXREAL_1:1;
( ['a,b'] = [.a,b.] & ['b,c'] = [.b,c.] ) by A1, INTEGRA5:def 3;
then ['a,c'] = ['a,b'] \/ ['b,c'] by A1, A10, XXREAL_1:165;
then f | ['a,c'] is bounded by A3, A4, RFUNCT_1:87;
hence integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) by A2, A7, A9, A11, INTEGRA6:17; :: thesis: verum