let n be Element of NAT ; :: thesis: for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let a, b, c, d be Real; :: thesis: for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
A2: now :: thesis: for i being Element of NAT st i in Seg n holds
integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d))
let i be Element of NAT ; :: thesis: ( i in Seg n implies integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),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;
A6: (proj (i,n)) * g is_integrable_on ['a,b'] by A3, A1;
(proj (i,n)) * (g | ['a,b']) is bounded by A3, A1;
then A7: ((proj (i,n)) * g) | ['a,b'] is bounded by RELAT_1:83;
A8: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A9: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
rng g c= dom (proj (i,n)) by A8;
then A10: ['a,b'] c= dom ((proj (i,n)) * g) by A1, RELAT_1:27;
A11: (proj (i,n)) * (f + g) = ((proj (i,n)) * f) + ((proj (i,n)) * g) by INTEGR15:15;
thus integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A4, A5, A9, A6, A7, A10, A1, A11, INTEGRA6:24; :: thesis: verum
end;
A12: now :: thesis: for i being Nat st i in dom (integral ((f + g),c,d)) holds
(integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i
let i be Nat; :: thesis: ( i in dom (integral ((f + g),c,d)) implies (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i )
assume i in dom (integral ((f + g),c,d)) ; :: thesis: (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i
then A13: i in Seg n by INTEGR15:def 18;
set P = proj (i,n);
thus (integral ((f + g),c,d)) . i = integral (((proj (i,n)) * (f + g)),c,d) by A13, INTEGR15:def 18
.= (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) by A13, A2
.= ((integral (f,c,d)) . i) + (integral (((proj (i,n)) * g),c,d)) by A13, INTEGR15:def 18
.= ((integral (f,c,d)) . i) + ((integral (g,c,d)) . i) by A13, INTEGR15:def 18
.= ((integral (f,c,d)) + (integral (g,c,d))) . i by RVSUM_1:11 ; :: thesis: verum
end;
A14: Seg n = dom (integral ((f + g),c,d)) by INTEGR15:def 18;
len ((integral (f,c,d)) + (integral (g,c,d))) = n by CARD_1:def 7;
then Seg n = dom ((integral (f,c,d)) + (integral (g,c,d))) by FINSEQ_1:def 3;
hence integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) by A14, A12, FINSEQ_1:13; :: thesis: verum