let n be Element of NAT ; :: thesis: for a, b, c being Real
for f being PartFunc of REAL,(REAL n) 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 a, b, c be Real; :: thesis: for f being PartFunc of REAL,(REAL n) 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 n); :: 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 A1: ( a <= b & f is_integrable_on ['a,b'] & 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)) )

A2: now :: thesis: for i being Element of NAT st i in Seg n holds
( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) )

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) )
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then dom ((proj (i,n)) * f) = dom f by RELAT_1:27;
hence ( (proj (i,n)) * f is_integrable_on ['a,c'] & (proj (i,n)) * f is_integrable_on ['c,b'] & integral (((proj (i,n)) * f),a,b) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) ) by A4, A5, A1, INTEGRA6:17; :: thesis: verum

end;

then for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['a,c'] ;
hence f is_integrable_on ['a,c'] ; :: thesis: ( f is_integrable_on ['c,b'] & integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) )
for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is_integrable_on ['c,b'] by A2;
hence f is_integrable_on ['c,b'] ; :: thesis: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b))

A6: now :: thesis: for i being Nat st i in dom (integral (f,a,b)) holds
(integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i

let i be Nat; :: thesis: ( i in dom (integral (f,a,b)) implies (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i )
assume i in dom (integral (f,a,b)) ; :: thesis: (integral (f,a,b)) . i = ((integral (f,a,c)) + (integral (f,c,b))) . i
then A7: i in Seg n by INTEGR15:def 18;
set P = proj (i,n);
thus (integral (f,a,b)) . i = integral (((proj (i,n)) * f),a,b) by A7, INTEGR15:def 18
.= (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,b)) by A7, A2
.= ((integral (f,a,c)) . i) + (integral (((proj (i,n)) * f),c,b)) by A7, INTEGR15:def 18
.= ((integral (f,a,c)) . i) + ((integral (f,c,b)) . i) by A7, INTEGR15:def 18
.= ((integral (f,a,c)) + (integral (f,c,b))) . i by RVSUM_1:11 ; :: thesis: verum

end;

A8: Seg n = dom (integral (f,a,b)) by INTEGR15:def 18;
len ((integral (f,a,c)) + (integral (f,c,b))) = n by CARD_1:def 7;
then Seg n = dom ((integral (f,a,c)) + (integral (f,c,b))) by FINSEQ_1:def 3;
hence integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A8, A6, FINSEQ_1:13; :: thesis: verum