let a, b, c be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['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 PartFunc of REAL,REAL; :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['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 that
A1: a <= b and
A2: f is_integrable_on ['a,b'] and
A3: ( f | ['a,b'] is bounded & ['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)) )
now :: thesis: ( b = c 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 A4: b = c ; :: 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 A5: ['c,b'] = [.c,b.] by INTEGRA5:def 3;
thus f is_integrable_on ['a,c'] by A2, A4; :: thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
['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 A5, INTEGRA1:5;
then A6: vol ['c,b'] = 0 by A4;
then f || ['c,b'] is integrable by INTEGRA4:6;
hence f is_integrable_on ['c,b'] ; :: thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))
integral (f,c,b) = integral (f,['c,b']) by A5, INTEGRA5:19;
then integral (f,c,b) = 0 by A6, INTEGRA4:6;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A4; :: thesis: verum
end;
hence ( f is_integrable_on ['a,c'] & f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) ) by A1, A2, A3, Lm2; :: thesis: verum