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 A1:
( 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 )
; :: 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) )
A2:
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 A1, RELAT_1:46;
:: thesis: verum
end;
A3:
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 B1:
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 P1:
(
A c= dom ((proj i,n) * f1) &
A c= dom ((proj i,n) * f2) )
by A2;
(
(proj i,n) * (f1 | A) is
bounded &
(proj i,n) * (f2 | A) is
bounded )
by A1, Defbounded, B1;
then P2:
(
((proj i,n) * f1) | A is
bounded &
((proj i,n) * f2) | A is
bounded )
by LMDEF, B1;
P3:
(
(proj i,n) * f1 is_integrable_on A &
(proj i,n) * f2 is_integrable_on A )
by B1, A1, Defintable;
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 INTEGRA6:11, P1, P2, P3;
:: 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 INTEGRA6:11, P1, P2, P3;
:: thesis: verum
end;
A4:
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 B1:
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 A3;
hence
(
(proj i,n) * (f1 + f2) is_integrable_on A &
(proj i,n) * (f1 - f2) is_integrable_on A )
by B1, Th31;
:: 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 Defintable; :: 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) )
for i being Element of NAT st i in Seg n holds
(proj i,n) * (f1 - f2) is_integrable_on A
by A4;
hence
f1 - f2 is_integrable_on A
by Defintable; :: thesis: ( 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
( ((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
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 &
(integral f2,A) . i = integral ((proj i,n) * f2),
A )
by DefintN;
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) )
;
:: thesis: verum
end;
A6:
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
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 ((proj i,n) * f1),A) + (integral ((proj i,n) * f2),A) = integral (((proj i,n) * f1) + ((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) &
(integral ((proj i,n) * f1),A) - (integral ((proj i,n) * f2),A) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),
A )
by A3, A5;
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 )
;
:: thesis: verum
end;
A7:
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 (((proj i,n) * f1) + ((proj i,n) * f2)),
A = integral ((proj i,n) * (f1 + f2)),
A &
((integral f1,A) . i) - ((integral f2,A) . i) = integral (((proj i,n) * f1) - ((proj i,n) * f2)),
A &
integral (((proj i,n) * f1) - ((proj i,n) * f2)),
A = integral ((proj i,n) * (f1 - f2)),
A )
by A6, Th31;
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 )
;
:: thesis: verum
end;
A8:
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
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 ((proj i,n) * (f1 + f2)),
A = (integral (f1 + f2),A) . i &
((integral f1,A) . i) - ((integral f2,A) . i) = integral ((proj i,n) * (f1 - f2)),
A &
integral ((proj i,n) * (f1 - f2)),
A = (integral (f1 - f2),A) . i )
by A7, DefintN;
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) )
;
:: thesis: verum
end;
C1:
( dom (integral (f1 + f2),A) = Seg n & dom ((integral f1,A) + (integral f2,A)) = Seg n & dom (integral (f1 - f2),A) = Seg n & dom ((integral f1,A) - (integral f2,A)) = Seg n )
by EUCLID:3;
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) &
((integral f1,A) + (integral f2,A)) . i = ((integral f1,A) . i) + ((integral f2,A) . i) )
by A8, RVSUM_1:27, C1;
hence
(integral (f1 + f2),A) . i = ((integral f1,A) + (integral f2,A)) . i
;
:: thesis: verum
end;
hence
integral (f1 + f2),A = (integral f1,A) + (integral f2,A)
by PARTFUN1:34, C1; :: thesis: integral (f1 - f2),A = (integral f1,A) - (integral f2,A)
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) &
((integral f1,A) - (integral f2,A)) . i = ((integral f1,A) . i) - ((integral f2,A) . i) )
by A8, RVSUM_1:48, C1;
hence
(integral (f1 - f2),A) . i = ((integral f1,A) - (integral f2,A)) . i
;
:: thesis: verum
end;
hence
integral (f1 - f2),A = (integral f1,A) - (integral f2,A)
by PARTFUN1:34, C1; :: thesis: verum