let X be RealNormSpace; :: thesis: for A being closed-interval Subset of REAL
for f, g, h being Function of A,the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
let A be closed-interval Subset of REAL ; :: thesis: for f, g, h being Function of A,the carrier of X st h = f + g & f is integrable & g is integrable holds
( h is integrable & integral h = (integral f) + (integral g) )
let f, g, h be Function of A,the carrier of X; :: thesis: ( h = f + g & f is integrable & g is integrable implies ( h is integrable & integral h = (integral f) + (integral g) ) )
assume AS: ( h = f + g & f is integrable & g is integrable ) ; :: thesis: ( h is integrable & integral h = (integral f) + (integral g) )
P01: ( dom h = A & dom f = A & dom g = A ) by FUNCT_2:def 1;
P0: now
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
( middle_sum h,S is convergent & lim (middle_sum h,S) = (integral f) + (integral g) )
let S be middle_volume_Sequence of h,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies ( middle_sum h,S is convergent & lim (middle_sum h,S) = (integral f) + (integral g) ) )
assume AS1: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum h,S is convergent & lim (middle_sum h,S) = (integral f) + (integral g) )
defpred S1[ Element of NAT , set ] means ex p being FinSequence of REAL st
( p = $2 & len p = len (T . $1) & ( for i being Nat st i in dom (T . $1) holds
( p . i in dom (h | (divset (T . $1),i)) & ex z being Point of X st
( z = (h | (divset (T . $1),i)) . (p . i) & (S . $1) . i = (vol (divset (T . $1),i)) * z ) ) ) );
P1: for k being Element of NAT ex p being Element of REAL * st S1[k,p]
proof
let k be Element of NAT ; :: thesis: ex p being Element of REAL * st S1[k,p]
defpred S2[ Nat, set ] means ( $2 in dom (h | (divset (T . k),$1)) & ex c being Point of X st
( c = (h | (divset (T . k),$1)) . $2 & (S . k) . $1 = (vol (divset (T . k),$1)) * c ) );
A1: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A2: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of REAL st S2[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of REAL st S2[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of REAL st S2[i,x]
then i in dom (T . k) by FINSEQ_1:def 3;
then consider c being Point of X such that
A21: ( c in rng (h | (divset (T . k),i)) & (S . k) . i = (vol (divset (T . k),i)) * c ) by Def5;
consider x being set such that
A22: ( x in dom (h | (divset (T . k),i)) & c = (h | (divset (T . k),i)) . x ) by A21, FUNCT_1:def 5;
( x in dom h & x in divset (T . k),i ) by A22, RELAT_1:86;
then reconsider x = x as Element of REAL ;
take x ; :: thesis: S2[i,x]
thus S2[i,x] by A21, A22; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A3: ( dom p = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S2[i,p . i] ) ) from FINSEQ_1:sch 5(A2);
 take p ; :: thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by A3, FINSEQ_1:def 3;
hence ( p is Element of REAL * & S1[k,p] ) by A3, A1, FINSEQ_1:def 11; :: thesis: verum
end;
consider F being Function of NAT ,(REAL * ) such that
P2: for x being Element of NAT holds S1[x,F . x] from FUNCT_2:sch 10(P1);
defpred S2[ Element of NAT , set ] means ex q being middle_volume of f,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Point of X st
( (F . $1) . i in dom (f | (divset (T . $1),i)) & z = (f | (divset (T . $1),i)) . ((F . $1) . i) & q . i = (vol (divset (T . $1),i)) * z ) ) );
P3: for k being Element of NAT ex y being Element of the carrier of X * st S2[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Element of the carrier of X * st S2[k,y]
defpred S3[ Nat, set ] means ex c being Point of X st
( (F . k) . $1 in dom (f | (divset (T . k),$1)) & c = (f | (divset (T . k),$1)) . ((F . k) . $1) & $2 = (vol (divset (T . k),$1)) * c );
A1: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A2: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of the carrier of X st S3[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S3[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of the carrier of X st S3[i,x]
then A21: i in dom (T . k) by FINSEQ_1:def 3;
consider p being FinSequence of REAL such that
A22: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset (T . k),i)) & ex z being Point of X st
( z = (h | (divset (T . k),i)) . (p . i) & (S . k) . i = (vol (divset (T . k),i)) * z ) ) ) ) by P2;
p . i in dom (h | (divset (T . k),i)) by A21, A22;
then A23: ( p . i in dom h & p . i in divset (T . k),i ) by RELAT_1:86;
then p . i in dom (f | (divset (T . k),i)) by RELAT_1:86, P01;
then (f | (divset (T . k),i)) . (p . i) in rng (f | (divset (T . k),i)) by FUNCT_1:12;
then reconsider x = (f | (divset (T . k),i)) . (p . i) as Element of the carrier of X ;
A24: (F . k) . i in dom (f | (divset (T . k),i)) by A22, A23, RELAT_1:86, P01;
(vol (divset (T . k),i)) * x is Element of the carrier of X ;
hence ex x being Element of the carrier of X st S3[i,x] by A22, A24; :: thesis: verum
end;
consider q being FinSequence of the carrier of X such that
A3: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S3[i,q . i] ) ) from FINSEQ_1:sch 5(A2);
 A4: len q = len (T . k) by A3, FINSEQ_1:def 3;
now
let i be Nat; :: thesis: ( i in dom (T . k) implies ex c being Point of X st
( c in rng (f | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c ) )
assume i in dom (T . k) ; :: thesis: ex c being Point of X st
( c in rng (f | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c )
then i in Seg (len (T . k)) by FINSEQ_1:def 3;
then consider c being Point of X such that
A41: ( (F . k) . i in dom (f | (divset (T . k),i)) & c = (f | (divset (T . k),i)) . ((F . k) . i) & q . i = (vol (divset (T . k),i)) * c ) by A3;
thus ex c being Point of X st
( c in rng (f | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c ) by A41, FUNCT_1:12; :: thesis: verum
end;
then reconsider q = q as middle_volume of f,T . k by A4, Def5;
q is Element of the carrier of X * by FINSEQ_1:def 11;
hence ex y being Element of the carrier of X * st S2[k,y] by A1, A3; :: thesis: verum
end;
consider Sf being Function of NAT ,(the carrier of X * ) such that
P4: for x being Element of NAT holds S2[x,Sf . x] from FUNCT_2:sch 10(P3);
now
let k be Element of NAT ; :: thesis: Sf . k is middle_volume of f,T . k
ex q being middle_volume of f,T . k st
( q = Sf . k & ( for i being Nat st i in dom (T . k) holds
ex z being Point of X st
( (F . k) . i in dom (f | (divset (T . k),i)) & z = (f | (divset (T . k),i)) . ((F . k) . i) & q . i = (vol (divset (T . k),i)) * z ) ) ) by P4;
hence Sf . k is middle_volume of f,T . k ; :: thesis: verum
end;
then reconsider Sf = Sf as middle_volume_Sequence of f,T by Def7;
defpred S3[ Element of NAT , set ] means ex q being middle_volume of g,T . $1 st
( q = $2 & ( for i being Nat st i in dom (T . $1) holds
ex z being Point of X st
( (F . $1) . i in dom (g | (divset (T . $1),i)) & z = (g | (divset (T . $1),i)) . ((F . $1) . i) & q . i = (vol (divset (T . $1),i)) * z ) ) );
P5: for k being Element of NAT ex y being Element of the carrier of X * st S3[k,y]
proof
let k be Element of NAT ; :: thesis: ex y being Element of the carrier of X * st S3[k,y]
defpred S4[ Nat, set ] means ex c being Point of X st
( (F . k) . $1 in dom (g | (divset (T . k),$1)) & c = (g | (divset (T . k),$1)) . ((F . k) . $1) & $2 = (vol (divset (T . k),$1)) * c );
A1: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A2: for i being Nat st i in Seg (len (T . k)) holds
ex x being Element of the carrier of X st S4[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len (T . k)) implies ex x being Element of the carrier of X st S4[i,x] )
assume i in Seg (len (T . k)) ; :: thesis: ex x being Element of the carrier of X st S4[i,x]
then A21: i in dom (T . k) by FINSEQ_1:def 3;
consider p being FinSequence of REAL such that
A22: ( p = F . k & len p = len (T . k) & ( for i being Nat st i in dom (T . k) holds
( p . i in dom (h | (divset (T . k),i)) & ex z being Point of X st
( z = (h | (divset (T . k),i)) . (p . i) & (S . k) . i = (vol (divset (T . k),i)) * z ) ) ) ) by P2;
p . i in dom (h | (divset (T . k),i)) by A21, A22;
then A23: ( p . i in dom h & p . i in divset (T . k),i ) by RELAT_1:86;
then p . i in dom (g | (divset (T . k),i)) by RELAT_1:86, P01;
then (g | (divset (T . k),i)) . (p . i) in rng (g | (divset (T . k),i)) by FUNCT_1:12;
then reconsider x = (g | (divset (T . k),i)) . (p . i) as Element of the carrier of X ;
A24: (F . k) . i in dom (g | (divset (T . k),i)) by A22, A23, RELAT_1:86, P01;
(vol (divset (T . k),i)) * x is Element of the carrier of X ;
hence ex x being Element of the carrier of X st S4[i,x] by A22, A24; :: thesis: verum
end;
consider q being FinSequence of the carrier of X such that
A3: ( dom q = Seg (len (T . k)) & ( for i being Nat st i in Seg (len (T . k)) holds
S4[i,q . i] ) ) from FINSEQ_1:sch 5(A2);
 A4: len q = len (T . k) by A3, FINSEQ_1:def 3;
now
let i be Nat; :: thesis: ( i in dom (T . k) implies ex c being Point of X st
( c in rng (g | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c ) )
assume i in dom (T . k) ; :: thesis: ex c being Point of X st
( c in rng (g | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c )
then i in Seg (len (T . k)) by FINSEQ_1:def 3;
then consider c being Point of X such that
A41: ( (F . k) . i in dom (g | (divset (T . k),i)) & c = (g | (divset (T . k),i)) . ((F . k) . i) & q . i = (vol (divset (T . k),i)) * c ) by A3;
thus ex c being Point of X st
( c in rng (g | (divset (T . k),i)) & q . i = (vol (divset (T . k),i)) * c ) by A41, FUNCT_1:12; :: thesis: verum
end;
then reconsider q = q as middle_volume of g,T . k by A4, Def5;
q is Element of the carrier of X * by FINSEQ_1:def 11;
hence ex y being Element of the carrier of X * st S3[k,y] by A1, A3; :: thesis: verum
end;
consider Sg being Function of NAT ,(the carrier of X * ) such that
P6: for x being Element of NAT holds S3[x,Sg . x] from FUNCT_2:sch 10(P5);
now
let k be Element of NAT ; :: thesis: Sg . k is middle_volume of g,T . k
ex q being middle_volume of g,T . k st
( q = Sg . k & ( for i being Nat st i in dom (T . k) holds
ex z being Point of X st
( (F . k) . i in dom (g | (divset (T . k),i)) & z = (g | (divset (T . k),i)) . ((F . k) . i) & q . i = (vol (divset (T . k),i)) * z ) ) ) by P6;
hence Sg . k is middle_volume of g,T . k ; :: thesis: verum
end;
then reconsider Sg = Sg as middle_volume_Sequence of g,T by Def7;
integral f is Point of X ;
then P7: ( middle_sum f,Sf is convergent & lim (middle_sum f,Sf) = integral f ) by Def14, AS, AS1;
integral g is Point of X ;
then P8: ( middle_sum g,Sg is convergent & lim (middle_sum g,Sg) = integral g ) by Def14, AS, AS1;
P9: (middle_sum f,Sf) + (middle_sum g,Sg) = middle_sum h,S
proof
now
let n be Element of NAT ; :: thesis: ((middle_sum f,Sf) . n) + ((middle_sum g,Sg) . n) = (middle_sum h,S) . n
consider p being FinSequence of REAL such that
A01: ( p = F . n & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p . i in dom (h | (divset (T . n),i)) & ex z being Point of X st
( z = (h | (divset (T . n),i)) . (p . i) & (S . n) . i = (vol (divset (T . n),i)) * z ) ) ) ) by P2;
consider q being middle_volume of f,T . n such that
A02: ( q = Sf . n & ( for i being Nat st i in dom (T . n) holds
ex z being Point of X st
( (F . n) . i in dom (f | (divset (T . n),i)) & z = (f | (divset (T . n),i)) . ((F . n) . i) & q . i = (vol (divset (T . n),i)) * z ) ) ) by P4;
consider r being middle_volume of g,T . n such that
A03: ( r = Sg . n & ( for i being Nat st i in dom (T . n) holds
ex z being Point of X st
( (F . n) . i in dom (g | (divset (T . n),i)) & z = (g | (divset (T . n),i)) . ((F . n) . i) & r . i = (vol (divset (T . n),i)) * z ) ) ) by P6;
A04: ( len (Sf . n) = len (T . n) & len (Sg . n) = len (T . n) & len (S . n) = len (T . n) ) by Def5;
A05: ( dom (Sf . n) = dom (T . n) & dom (Sg . n) = dom (T . n) & dom (S . n) = dom (T . n) ) by A04, FINSEQ_3:31;
now
let i be Nat; :: thesis: ( 1 <= i & i <= len (S . n) implies (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i) )
assume ( 1 <= i & i <= len (S . n) ) ; :: thesis: (S . n) /. i = ((Sf . n) /. i) + ((Sg . n) /. i)
then i in Seg (len (S . n)) by FINSEQ_1:3;
then K001: i in dom (S . n) by FINSEQ_1:def 3;
consider t being Point of X such that
K002: ( t = (h | (divset (T . n),i)) . ((F . n) . i) & (S . n) . i = (vol (divset (T . n),i)) * t ) by K001, A05, A01;
consider z being Point of X such that
K003: ( (F . n) . i in dom (f | (divset (T . n),i)) & z = (f | (divset (T . n),i)) . ((F . n) . i) & q . i = (vol (divset (T . n),i)) * z ) by A02, K001, A05;
consider w being Point of X such that
K004: ( (F . n) . i in dom (g | (divset (T . n),i)) & w = (g | (divset (T . n),i)) . ((F . n) . i) & r . i = (vol (divset (T . n),i)) * w ) by A03, K001, A05;
K005: (F . n) . i in divset (T . n),i by K004, RELAT_1:86;
K006: (F . n) . i in dom g by K004, RELAT_1:86;
K007: (F . n) . i in A by K004;
then K008: (F . n) . i in dom h by FUNCT_2:def 1;
K009: (F . n) . i in dom f by K007, FUNCT_2:def 1;
K010: f /. ((F . n) . i) = f . ((F . n) . i) by PARTFUN1:def 8, K009
.= z by K003, K005, FUNCT_1:72 ;
K011: g /. ((F . n) . i) = g . ((F . n) . i) by PARTFUN1:def 8, K006
.= w by K004, K005, FUNCT_1:72 ;
K012: t = (h | (divset (T . n),i)) . ((F . n) . i) by K002
.= h . ((F . n) . i) by K005, FUNCT_1:72
.= h /. ((F . n) . i) by PARTFUN1:def 8, K008
.= (f /. ((F . n) . i)) + (g /. ((F . n) . i)) by VFUNCT_1:def 1, K008, AS
.= z + w by K010, K011 ;
K013: (vol (divset (T . n),i)) * z = (Sf . n) . i by K003, A02
.= (Sf . n) /. i by K001, A05, PARTFUN1:def 8 ;
K014: (vol (divset (T . n),i)) * w = (Sg . n) . i by K004, A03
.= (Sg . n) /. i by K001, A05, PARTFUN1:def 8 ;
thus (S . n) /. i = (S . n) . i by K001, PARTFUN1:def 8
.= (vol (divset (T . n),i)) * t by K002
.= ((vol (divset (T . n),i)) * z) + ((vol (divset (T . n),i)) * w) by K012, RLVECT_1:def 8
.= ((Sf . n) /. i) + ((Sg . n) /. i) by K013, K014 ; :: thesis: verum
end;
then A06: (Sf . n) + (Sg . n) = S . n by BINOM:def 4, A05;
thus ((middle_sum f,Sf) . n) + ((middle_sum g,Sg) . n) = (middle_sum f,(Sf . n)) + ((middle_sum g,Sg) . n) by Def8
.= (middle_sum f,(Sf . n)) + (middle_sum g,(Sg . n)) by Def8
.= (Sum (Sf . n)) + (middle_sum g,(Sg . n))
.= (Sum (Sf . n)) + (Sum (Sg . n))
.= Sum (S . n) by A06, A04, SM1
.= middle_sum h,(S . n)
.= (middle_sum h,S) . n by Def8 ; :: thesis: verum
end;
hence (middle_sum f,Sf) + (middle_sum g,Sg) = middle_sum h,S by NORMSP_1:def 5; :: thesis: verum
end;
hence middle_sum h,S is convergent by P7, P8, NORMSP_1:34; :: thesis: lim (middle_sum h,S) = (integral f) + (integral g)
thus lim (middle_sum h,S) = (integral f) + (integral g) by P7, P8, P9, NORMSP_1:42; :: thesis: verum
end;
hence h is integrable by Def13; :: thesis: integral h = (integral f) + (integral g)
hence integral h = (integral f) + (integral g) by Def14, P0; :: thesis: verum