let f be Function 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 & f | ['b,c'] is bounded ) and
A4: ( f is_integrable_on ['a,b'] & 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)) )
reconsider ff = f as PartFunc of REAL,REAL ;
( ['a,c'] c= dom ff & ff | ['a,b'] is bounded & ff | ['b,c'] is bounded & ff is_integrable_on ['a,b'] & ff is_integrable_on ['b,c'] ) by A2, A3, A4;
hence ( f is_integrable_on ['a,c'] & integral (f,a,c) = (integral (f,a,b)) + (integral (f,b,c)) ) by INTEGR24:1, A1; :: thesis: verum