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 and
A4: ['a,b'] c= dom f and
A5: 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 A6: 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 A7: ['c,b'] = [.c,b.] by INTEGRA5:def 4;
thus f is_integrable_on ['a,c'] by A2, A6; :: thesis: ( f is_integrable_on ['c,b'] & integral f,a,b = (integral f,a,c) + (integral f,c,b) )
['c,b'] = [.(inf ['c,b']),(sup ['c,b']).] by INTEGRA1:5;
then ( inf ['c,b'] = c & sup ['c,b'] = b ) by A7, INTEGRA1:6;
then A8: vol ['c,b'] = 0 by A6;
then ( f || ['c,b'] is integrable & integral (f || ['c,b']) = 0 ) 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 A7, INTEGRA5:19;
then integral f,c,b = 0 by A8, INTEGRA4:6;
hence integral f,a,b = (integral f,a,c) + (integral f,c,b) by A6; :: 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, A4, A5, Lm2; :: thesis: verum