let n be Element of NAT ; :: thesis: for A being non empty 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 non empty 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:27; :: 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;
then A9: ((proj (i,n)) * f2) | A is bounded by Lm6;
(proj (i,n)) * (f1 | A) is bounded by A3, A7;
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;
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 ; :: 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 ; :: 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 FINSEQ_1:89;
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:11; :: thesis: verum
end;
dom ((integral (f1,A)) + (integral (f2,A))) = Seg n by FINSEQ_1:89;
hence integral ((f1 + f2),A) = (integral (f1,A)) + (integral (f2,A)) by A21, FINSEQ_1:89, PARTFUN1:5; :: thesis: integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A))
A22: dom (integral ((f1 - f2),A)) = Seg n by FINSEQ_1:89;
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:27; :: thesis: verum
end;
dom ((integral (f1,A)) - (integral (f2,A))) = Seg n by FINSEQ_1:89;
hence integral ((f1 - f2),A) = (integral (f1,A)) - (integral (f2,A)) by A23, FINSEQ_1:89, PARTFUN1:5; :: thesis: verum