let a, b, c be Real; 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; ( 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'] )
; ( 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 ( 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
;
( 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;
( 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']
;
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;
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; verum