let a, b, c be Real; :: thesis: for f being Function of REAL,REAL st a < b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded holds
( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )
let f be Function of REAL,REAL; :: thesis: ( a < b & b < c & f is_integrable_on ['a,c'] & f | ['a,c'] is bounded implies ( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) ) )
assume A1: ( a < b & b < c ) ; :: thesis: ( not f is_integrable_on ['a,c'] or not f | ['a,c'] is bounded or ( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) ) )
then AD: a <= c by XXREAL_0:2;
assume A2: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded ) ; :: thesis: ( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) )
reconsider F = f as PartFunc of REAL,REAL ;
A6: REAL = dom f by FUNCT_2:def 1;
b in [.a,c.] by A1;
then A9: b in ['a,c'] by A1, INTEGRA5:def 3, XXREAL_0:2;
( F is_integrable_on ['a,c'] & F | ['a,c'] is bounded ) by A2;
hence ( f is_integrable_on ['a,b'] & f is_integrable_on ['b,c'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) ) by A6, A9, INTEGRA6:17, INTEGRA6:18, AD, A1; :: thesis: verum