let a, b, c be real number ; :: 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

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 4;
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:5;
then ( lower_bound ['c,b'] = c & upper_bound ['c,b'] = b ) by A5, INTEGRA1:6;
then A6: vol ['c,b'] = 0 by A4;
then f || ['c,b'] is integrable by INTEGRA4:6;
hence f is_integrable_on ['c,b'] by INTEGRA5:def 2; :: thesis: integral f,a,b = (integral f,a,c) + (integral f,c,b)
( c is Real & b is Real ) by XREAL_0:def 1;
then 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