let n be Element of NAT ; :: thesis: for a, b, c, d 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'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let a, b, c, d 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'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
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'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))

A2: now :: thesis: for i being Element of NAT st i in Seg n holds
integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d))

let i be Element of NAT ; :: thesis: ( i in Seg n implies integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d))
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 integral (((proj (i,n)) * f),a,d) = (integral (((proj (i,n)) * f),a,c)) + (integral (((proj (i,n)) * f),c,d)) by A4, A5, A1, INTEGRA6:20; :: thesis: verum

end;

A6: Seg n = dom (integral (f,a,d)) by INTEGR15:def 18;

A7: now :: thesis: for i0 being Nat st i0 in dom (integral (f,a,d)) holds
(integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0

let i0 be Nat; :: thesis: ( i0 in dom (integral (f,a,d)) implies (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0 )
assume A8: i0 in dom (integral (f,a,d)) ; :: thesis: (integral (f,a,d)) . i0 = ((integral (f,a,c)) + (integral (f,c,d))) . i0
set P = proj (i0,n);
thus (integral (f,a,d)) . i0 = integral (((proj (i0,n)) * f),a,d) by A8, A6, INTEGR15:def 18
.= (integral (((proj (i0,n)) * f),a,c)) + (integral (((proj (i0,n)) * f),c,d)) by A8, A2, A6
.= ((integral (f,a,c)) . i0) + (integral (((proj (i0,n)) * f),c,d)) by A8, A6, INTEGR15:def 18
.= ((integral (f,a,c)) . i0) + ((integral (f,c,d)) . i0) by A8, A6, INTEGR15:def 18
.= ((integral (f,a,c)) + (integral (f,c,d))) . i0 by RVSUM_1:11 ; :: thesis: verum

end;

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