let n be Element of NAT ; :: thesis: for A being closed-interval Subset of REAL
for f1, f2 being PartFunc of REAL ,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )
let A be closed-interval Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,(REAL n) st f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded holds
( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )
let f1, f2 be PartFunc of REAL ,(REAL n); :: thesis: ( f1 is_integrable_on A & f2 is_integrable_on A & A c= dom f1 & A c= dom f2 & f1 | A is bounded & f2 | A is bounded implies ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) ) )
assume that
A1: ( f1 is_integrable_on A & f2 is_integrable_on A ) and
A2: ( A c= dom f1 & A c= dom f2 ) and
A3: f1 | A is bounded and
A4: f2 | A is bounded ; :: thesis: ( f1 + f2 is_integrable_on A & f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )
A5: for i being Element of NAT st i in Seg n holds
( A c= dom ((proj i,n) * f1) & A c= dom ((proj i,n) * f2) )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( A c= dom ((proj i,n) * f1) & A c= dom ((proj i,n) * f2) ) )
assume i in Seg n ; :: thesis: ( A c= dom ((proj i,n) * f1) & A c= dom ((proj i,n) * f2) )
dom (proj i,n) = REAL n by FUNCT_2:def 1;
then ( rng f1 c= dom (proj i,n) & rng f2 c= dom (proj i,n) ) ;
hence ( A c= dom ((proj i,n) * f1) & A c= dom ((proj i,n) * f2) ) by A2, RELAT_1:46; :: thesis: verum

end;

A6: for i being Element of NAT st i in Seg n holds
( ((proj i,n) * f1) + ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) + ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) - ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( ((proj i,n) * f1) + ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) + ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) - ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) ) )
assume A7: i in Seg n ; :: thesis: ( ((proj i,n) * f1) + ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) + ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) - ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) )
then A8: ( A c= dom ((proj i,n) * f1) & A c= dom ((proj i,n) * f2) ) by A5;
(proj i,n) * (f2 | A) is bounded by A4, A7, Def15;
then A9: ((proj i,n) * f2) | A is bounded by Lm6;
(proj i,n) * (f1 | A) is bounded by A3, A7, Def15;
then A10: ((proj i,n) * f1) | A is bounded by Lm6;
A11: ( (proj i,n) * f1 is_integrable_on A & (proj i,n) * f2 is_integrable_on A ) by A1, A7, Def16;
hence ( ((proj i,n) * f1) + ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) + ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) ) by A8, A10, A9, INTEGRA6:11; :: thesis: ( ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) - ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) )
thus ( ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A & integral (((proj i,n) * f1) - ((proj i,n) * f2)),A = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) ) by A8, A10, A9, A11, INTEGRA6:11; :: thesis: verum

end;

A12: for i being Element of NAT st i in Seg n holds
( (proj i,n) * (f1 + f2) is_integrable_on A & (proj i,n) * (f1 - f2) is_integrable_on A )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (proj i,n) * (f1 + f2) is_integrable_on A & (proj i,n) * (f1 - f2) is_integrable_on A ) )
assume i in Seg n ; :: thesis: ( (proj i,n) * (f1 + f2) is_integrable_on A & (proj i,n) * (f1 - f2) is_integrable_on A )
then ( ((proj i,n) * f1) + ((proj i,n) * f2) is_integrable_on A & ((proj i,n) * f1) - ((proj i,n) * f2) is_integrable_on A ) by A6;
hence ( (proj i,n) * (f1 + f2) is_integrable_on A & (proj i,n) * (f1 - f2) is_integrable_on A ) by Th15; :: thesis: verum

end;

then for i being Element of NAT st i in Seg n holds
(proj i,n) * (f1 + f2) is_integrable_on A ;
hence f1 + f2 is_integrable_on A by Def16; :: thesis: ( f1 - f2 is_integrable_on A & integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )
A13: for i being Element of NAT st i in Seg n holds
( ((integral f1,A) . i) + ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((integral f1,A) . i) - ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( ((integral f1,A) . i) + ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((integral f1,A) . i) - ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) ) )
assume A14: i in Seg n ; :: thesis: ( ((integral f1,A) . i) + ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((integral f1,A) . i) - ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) )
then (integral f1,A) . i = integral ((proj i,n) * f1),A by Def17;
hence ( ((integral f1,A) . i) + ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((integral f1,A) . i) - ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) ) by A14, Def17; :: thesis: verum

end;

A15: for i being Element of NAT st i in Seg n holds
( ((integral f1,A) . i) + ((integral f2,A) . i) = integral (((proj i,n) * f1) + ((proj i,n) * f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),A )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral (((proj i,n) * f1) + ((proj i,n) * f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),A ) )
assume A16: i in Seg n ; :: thesis: ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral (((proj i,n) * f1) + ((proj i,n) * f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),A )
then ( ((integral f1,A) . i) + ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) & ((integral f1,A) . i) - ((integral f2,A) . i) = (integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) ) by A13;
hence ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral (((proj i,n) * f1) + ((proj i,n) * f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),A ) by A6, A16; :: thesis: verum

end;

A17: for i being Element of NAT st i in Seg n holds
( ((integral f1,A) . i) + ((integral f2,A) . i) = integral ((proj i,n) * (f1 + f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),A )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral ((proj i,n) * (f1 + f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),A ) )
assume i in Seg n ; :: thesis: ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral ((proj i,n) * (f1 + f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),A )
then ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral (((proj i,n) * f1) + ((proj i,n) * f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),A ) by A15;
hence ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral ((proj i,n) * (f1 + f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),A ) by Th15; :: thesis: verum

end;

A18: for i being Element of NAT st i in Seg n holds
( (integral (f1 + f2),A) . i = ((integral f1,A) . i) + ((integral f2,A) . i) & (integral (f1 - f2),A) . i = ((integral f1,A) . i) - ((integral f2,A) . i) )

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ( (integral (f1 + f2),A) . i = ((integral f1,A) . i) + ((integral f2,A) . i) & (integral (f1 - f2),A) . i = ((integral f1,A) . i) - ((integral f2,A) . i) ) )
assume A19: i in Seg n ; :: thesis: ( (integral (f1 + f2),A) . i = ((integral f1,A) . i) + ((integral f2,A) . i) & (integral (f1 - f2),A) . i = ((integral f1,A) . i) - ((integral f2,A) . i) )
then ( ((integral f1,A) . i) + ((integral f2,A) . i) = integral ((proj i,n) * (f1 + f2)),A & ((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),A ) by A17;
hence ( (integral (f1 + f2),A) . i = ((integral f1,A) . i) + ((integral f2,A) . i) & (integral (f1 - f2),A) . i = ((integral f1,A) . i) - ((integral f2,A) . i) ) by A19, Def17; :: thesis: verum

end;

for i being Element of NAT st i in Seg n holds
(proj i,n) * (f1 - f2) is_integrable_on A by A12;
hence f1 - f2 is_integrable_on A by Def16; :: thesis: ( integral (f1 + f2),A = (integral f1,A) + (integral f2,A) & integral (f1 - f2),A = (integral f1,A) - (integral f2,A) )
A20: dom (integral (f1 + f2),A) = Seg n by EUCLID:3;
A21: for i being Element of NAT st i in dom (integral (f1 + f2),A) holds
(integral (f1 + f2),A) . i = ((integral f1,A) + (integral f2,A)) . i

proof

let i be Element of NAT ; :: thesis: ( i in dom (integral (f1 + f2),A) implies (integral (f1 + f2),A) . i = ((integral f1,A) + (integral f2,A)) . i )
assume i in dom (integral (f1 + f2),A) ; :: thesis: (integral (f1 + f2),A) . i = ((integral f1,A) + (integral f2,A)) . i
then (integral (f1 + f2),A) . i = ((integral f1,A) . i) + ((integral f2,A) . i) by A18, A20;
hence (integral (f1 + f2),A) . i = ((integral f1,A) + (integral f2,A)) . i by RVSUM_1:27; :: thesis: verum

end;

dom ((integral f1,A) + (integral f2,A)) = Seg n by EUCLID:3;
hence integral (f1 + f2),A = (integral f1,A) + (integral f2,A) by A21, EUCLID:3, PARTFUN1:34; :: thesis: integral (f1 - f2),A = (integral f1,A) - (integral f2,A)
A22: dom (integral (f1 - f2),A) = Seg n by EUCLID:3;
A23: for i being Element of NAT st i in dom (integral (f1 - f2),A) holds
(integral (f1 - f2),A) . i = ((integral f1,A) - (integral f2,A)) . i

proof

let i be Element of NAT ; :: thesis: ( i in dom (integral (f1 - f2),A) implies (integral (f1 - f2),A) . i = ((integral f1,A) - (integral f2,A)) . i )
assume i in dom (integral (f1 - f2),A) ; :: thesis: (integral (f1 - f2),A) . i = ((integral f1,A) - (integral f2,A)) . i
then (integral (f1 - f2),A) . i = ((integral f1,A) . i) - ((integral f2,A) . i) by A18, A22;
hence (integral (f1 - f2),A) . i = ((integral f1,A) - (integral f2,A)) . i by RVSUM_1:48; :: thesis: verum

end;

dom ((integral f1,A) - (integral f2,A)) = Seg n by EUCLID:3;
hence integral (f1 - f2),A = (integral f1,A) - (integral f2,A) by A23, EUCLID:3, PARTFUN1:34; :: thesis: verum