let X be RealBanachSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
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
let A be non empty closed_interval Subset of REAL; :: thesis: for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
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
let h be Function of A, the carrier of X; :: thesis: ( ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) implies for T being DivSequence of A
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 )
assume A1: for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ; :: thesis: for T being DivSequence of A
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
thus for T being DivSequence of A
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 :: thesis: verum
proof
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
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 )
assume A2: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: middle_sum (h,S) is convergent
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 ) ) ) );
A3: 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 ) );
A4: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A5: 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
A6: ( c in rng (h | (divset ((T . k),i))) & (S . k) . i = (vol (divset ((T . k),i))) * c ) by INTEGR18:def 1;
consider x being object such that
A7: ( x in dom (h | (divset ((T . k),i))) & c = (h | (divset ((T . k),i))) . x ) by A6, FUNCT_1:def 3;
( x in dom h & x in divset ((T . k),i) ) by A7, RELAT_1:57;
then reconsider x = x as Element of REAL ;
take x ; :: thesis: S2[i,x]
thus S2[i,x] by A6, A7; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A8: ( 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(A5);
 take p ; :: thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by A8, FINSEQ_1:def 3;
hence ( p is Element of REAL * & S1[k,p] ) by A8, A4, FINSEQ_1:def 11; :: thesis: verum
end;
consider Fn being sequence of (REAL *) such that
A9: for x being Element of NAT holds S1[x,Fn . x] from FUNCT_2:sch 3(A3);
 consider Fm being sequence of (REAL *) such that
A10: for x being Element of NAT holds S1[x,Fm . x] from FUNCT_2:sch 3(A3);
 A11: 0 <= vol A by INTEGRA1:9;
now :: thesis: for p being Real st p > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p
let p be Real; :: thesis: ( p > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p )
set pp2 = p / 2;
set pv = (p / 2) / ((vol A) + 1);
assume p > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p
then A12: ( 0 < p / 2 & p / 2 < p ) by XREAL_1:215, XREAL_1:216;
then A13: 0 < (p / 2) / ((vol A) + 1) by A11, XREAL_1:139;
then ((p / 2) / ((vol A) + 1)) * (vol A) < ((p / 2) / ((vol A) + 1)) * ((vol A) + 1) by XREAL_1:29, XREAL_1:68;
then ((p / 2) / ((vol A) + 1)) * (vol A) < p / 2 by A11, XCMPLX_1:87;
then A14: ((p / 2) / ((vol A) + 1)) * (vol A) < p by A12, XXREAL_0:2;
set p2v = ((p / 2) / ((vol A) + 1)) / 2;
consider sk being Real such that
A15: ( 0 < sk & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < sk holds
||.((h /. x1) - (h /. x2)).|| < ((p / 2) / ((vol A) + 1)) / 2 ) ) by A1, A13, XREAL_1:215;
consider k being Nat such that
A16: for i being Nat st k <= i holds
|.(((delta T) . i) - 0).| < sk by A15, A2, SEQ_2:def 7;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p )
A17: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
assume ( n >= k & m >= k ) ; :: thesis: ||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p
then ( |.(((delta T) . n) - 0).| < sk & |.(((delta T) . m) - 0).| < sk ) by A16;
then ( |.(delta (T . n)).| < sk & |.(delta (T . m)).| < sk ) by INTEGRA3:def 2, A17;
then A18: ( delta (T . n) < sk & delta (T . m) < sk ) by INTEGRA3:9, ABSVALUE:def 1;
A19: ( (middle_sum (h,S)) . n = middle_sum (h,(S . n)) & (middle_sum (h,S)) . m = middle_sum (h,(S . m)) ) by INTEGR18:def 4;
consider p1 being FinSequence of REAL such that
A20: ( p1 = Fn . n & len p1 = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p1 . i in dom (h | (divset ((T . n),i))) & ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) ) ) ) by A9, A17;
consider p2 being FinSequence of REAL such that
A21: ( p2 = Fm . m & len p2 = len (T . m) & ( for i being Nat st i in dom (T . m) holds
( p2 . i in dom (h | (divset ((T . m),i))) & ex z being Point of X st
( z = (h | (divset ((T . m),i))) . (p2 . i) & (S . m) . i = (vol (divset ((T . m),i))) * z ) ) ) ) by A10, A17;
defpred S2[ object , object , object ] means ex i, j being Nat ex z being Point of X st
( $1 = i & $2 = j & z = (h | (divset ((T . n),i))) . (p1 . i) & $3 = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z );
A22: for x, y being object st x in Seg (len (T . n)) & y in Seg (len (T . m)) holds
ex w being object st
( w in the carrier of X & S2[x,y,w] )
proof
let x, y be object ; :: thesis: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) implies ex w being object st
( w in the carrier of X & S2[x,y,w] ) )
assume A23: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) ) ; :: thesis: ex w being object st
( w in the carrier of X & S2[x,y,w] )
then reconsider i = x, j = y as Nat ;
i in dom (T . n) by FINSEQ_1:def 3, A23;
then consider z being Point of X such that
A24: ( z = (h | (divset ((T . n),i))) . (p1 . i) & (S . n) . i = (vol (divset ((T . n),i))) * z ) by A20;
(xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z in the carrier of X ;
hence ex w being object st
( w in the carrier of X & S2[x,y,w] ) by A24; :: thesis: verum
end;
consider Snm being Function of [:(Seg (len (T . n))),(Seg (len (T . m))):], the carrier of X such that
A25: for x, y being object st x in Seg (len (T . n)) & y in Seg (len (T . m)) holds
S2[x,y,Snm . (x,y)] from BINOP_1:sch 1(A22);
A26: for i, j being Nat st i in Seg (len (T . n)) & j in Seg (len (T . m)) holds
ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
proof
let i, j be Nat; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) )
assume ( i in Seg (len (T . n)) & j in Seg (len (T . m)) ) ; :: thesis: ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
then ex i1, j1 being Nat ex z being Point of X st
( i = i1 & j = j1 & z = (h | (divset ((T . n),i1))) . (p1 . i1) & Snm . (i,j) = (xvol ((divset ((T . n),i1)) /\ (divset ((T . m),j1)))) * z ) by A25;
hence ex z being Point of X st
( z = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) ; :: thesis: verum
end;
defpred S3[ Nat, object ] means ex r being FinSequence of X st
( dom r = Seg (len (T . m)) & $2 = Sum r & ( for j being Nat st j in dom r holds
r . j = Snm . ($1,j) ) );
A27: for k being Nat st k in Seg (len (T . n)) holds
ex x being object st S3[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len (T . n)) implies ex x being object st S3[k,x] )
assume A28: k in Seg (len (T . n)) ; :: thesis: ex x being object st S3[k,x]
deffunc H1( set ) -> set = Snm . (k,$1);
consider r being FinSequence such that
A29: len r = len (T . m) and
A30: for j being Nat st j in dom r holds
r . j = H1(j) from FINSEQ_1:sch 2();
 A31: dom r = Seg (len (T . m)) by A29, FINSEQ_1:def 3;
for j being Nat st j in dom r holds
r . j in the carrier of X
proof
let j be Nat; :: thesis: ( j in dom r implies r . j in the carrier of X )
assume A32: j in dom r ; :: thesis: r . j in the carrier of X
then [k,j] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A31, A28, ZFMISC_1:87;
then Snm . (k,j) in the carrier of X by FUNCT_2:5;
hence r . j in the carrier of X by A30, A32; :: thesis: verum
end;
then reconsider r = r as FinSequence of X by FINSEQ_2:12;
take x = Sum r; :: thesis: S3[k,x]
thus S3[k,x] by A30, A31; :: thesis: verum
end;
consider Xp being FinSequence such that
A33: ( dom Xp = Seg (len (T . n)) & ( for k being Nat st k in Seg (len (T . n)) holds
S3[k,Xp . k] ) ) from FINSEQ_1:sch 1(A27);
 for i being Nat st i in dom Xp holds
Xp . i in the carrier of X
proof
let i be Nat; :: thesis: ( i in dom Xp implies Xp . i in the carrier of X )
assume i in dom Xp ; :: thesis: Xp . i in the carrier of X
then ex r being FinSequence of X st
( dom r = Seg (len (T . m)) & Xp . i = Sum r & ( for j being Nat st j in dom r holds
r . j = Snm . (i,j) ) ) by A33;
hence Xp . i in the carrier of X ; :: thesis: verum
end;
then reconsider Xp = Xp as FinSequence of X by FINSEQ_2:12;
A34: len Xp = len (T . n) by FINSEQ_1:def 3, A33;
for k being Nat st 1 <= k & k <= len Xp holds
Xp . k = (S . n) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len Xp implies Xp . k = (S . n) . k )
assume ( 1 <= k & k <= len Xp ) ; :: thesis: Xp . k = (S . n) . k
then A35: ( k in Seg (len Xp) & k in Seg (len (T . n)) ) by A34;
then A36: ( k in dom Xp & k in dom (T . n) ) by FINSEQ_1:def 3;
then consider z being Point of X such that
A37: ( z = (h | (divset ((T . n),k))) . (p1 . k) & (S . n) . k = (vol (divset ((T . n),k))) * z ) by A20;
consider r being FinSequence of X such that
A38: ( dom r = Seg (len (T . m)) & Xp . k = Sum r & ( for j being Nat st j in dom r holds
r . j = Snm . (k,j) ) ) by A35, A33;
defpred S4[ Nat, set ] means $2 = xvol ((divset ((T . n),k)) /\ (divset ((T . m),$1)));
A39: for i being Nat st i in Seg (len r) holds
ex x being Element of REAL st S4[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len r) implies ex x being Element of REAL st S4[i,x] )
assume i in Seg (len r) ; :: thesis: ex x being Element of REAL st S4[i,x]
xvol ((divset ((T . n),k)) /\ (divset ((T . m),i))) in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S4[i,x] ; :: thesis: verum
end;
consider vtntm being FinSequence of REAL such that
A40: ( dom vtntm = Seg (len r) & ( for i being Nat st i in Seg (len r) holds
S4[i,vtntm . i] ) ) from FINSEQ_1:sch 5(A39);
 A41: ( dom vtntm = dom r & ( for j being Nat st j in dom vtntm holds
vtntm . j = xvol ((divset ((T . n),k)) /\ (divset ((T . m),j))) ) ) by A40, FINSEQ_1:def 3;
A42: ( len vtntm = len r & len (T . m) = len r ) by A38, A40, FINSEQ_1:def 3;
then A43: Sum vtntm = vol (divset ((T . n),k)) by Th8, A40, A36, INTEGRA1:8;
for j being Nat st j in dom r holds
ex x being Real st
( x = vtntm . j & r . j = x * z )
proof
let j be Nat; :: thesis: ( j in dom r implies ex x being Real st
( x = vtntm . j & r . j = x * z ) )
assume A44: j in dom r ; :: thesis: ex x being Real st
( x = vtntm . j & r . j = x * z )
then A45: ex w being Point of X st
( w = (h | (divset ((T . n),k))) . (p1 . k) & Snm . (k,j) = (xvol ((divset ((T . n),k)) /\ (divset ((T . m),j)))) * w ) by A26, A35, A38;
take vtntm . j ; :: thesis: ( vtntm . j = vtntm . j & r . j = (vtntm . j) * z )
r . j = (xvol ((divset ((T . n),k)) /\ (divset ((T . m),j)))) * z by A37, A45, A44, A38;
hence ( vtntm . j = vtntm . j & r . j = (vtntm . j) * z ) by A41, A44; :: thesis: verum
end;
hence Xp . k = (S . n) . k by A37, A38, A43, Th7, A42; :: thesis: verum
end;
then A46: Xp = S . n by INTEGR18:def 1, A34;
defpred S4[ Nat, object ] means ex s being FinSequence of X st
( dom s = Seg (len (T . n)) & $2 = Sum s & ( for i being Nat st i in dom s holds
s . i = Snm . (i,$1) ) );
A47: for k being Nat st k in Seg (len (T . m)) holds
ex x being object st S4[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len (T . m)) implies ex x being object st S4[k,x] )
assume A48: k in Seg (len (T . m)) ; :: thesis: ex x being object st S4[k,x]
deffunc H1( set ) -> set = Snm . ($1,k);
consider s being FinSequence such that
A49: len s = len (T . n) and
A50: for i being Nat st i in dom s holds
s . i = H1(i) from FINSEQ_1:sch 2();
 A51: dom s = Seg (len (T . n)) by A49, FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in the carrier of X
proof
let i be Nat; :: thesis: ( i in dom s implies s . i in the carrier of X )
assume A52: i in dom s ; :: thesis: s . i in the carrier of X
then [i,k] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A51, A48, ZFMISC_1:87;
then Snm . (i,k) in the carrier of X by FUNCT_2:5;
hence s . i in the carrier of X by A50, A52; :: thesis: verum
end;
then reconsider s = s as FinSequence of X by FINSEQ_2:12;
take x = Sum s; :: thesis: S4[k,x]
thus S4[k,x] by A50, A51; :: thesis: verum
end;
consider Xq being FinSequence such that
A53: ( dom Xq = Seg (len (T . m)) & ( for k being Nat st k in Seg (len (T . m)) holds
S4[k,Xq . k] ) ) from FINSEQ_1:sch 1(A47);
 for j being Nat st j in dom Xq holds
Xq . j in the carrier of X
proof
let j be Nat; :: thesis: ( j in dom Xq implies Xq . j in the carrier of X )
assume j in dom Xq ; :: thesis: Xq . j in the carrier of X
then ex s being FinSequence of X st
( dom s = Seg (len (T . n)) & Xq . j = Sum s & ( for i being Nat st i in dom s holds
s . i = Snm . (i,j) ) ) by A53;
hence Xq . j in the carrier of X ; :: thesis: verum
end;
then reconsider Xq = Xq as FinSequence of X by FINSEQ_2:12;
defpred S5[ object , object , object ] means ex i, j being Nat ex z being Point of X st
( $1 = i & $2 = j & z = (h | (divset ((T . m),j))) . (p2 . j) & $3 = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z );
A54: for x, y being object st x in Seg (len (T . n)) & y in Seg (len (T . m)) holds
ex w being object st
( w in the carrier of X & S5[x,y,w] )
proof
let x, y be object ; :: thesis: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) implies ex w being object st
( w in the carrier of X & S5[x,y,w] ) )
assume A55: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) ) ; :: thesis: ex w being object st
( w in the carrier of X & S5[x,y,w] )
then reconsider i = x, j = y as Nat ;
j in dom (T . m) by FINSEQ_1:def 3, A55;
then consider z being Point of X such that
A56: ( z = (h | (divset ((T . m),j))) . (p2 . j) & (S . m) . j = (vol (divset ((T . m),j))) * z ) by A21;
(xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z in the carrier of X ;
hence ex w being object st
( w in the carrier of X & S5[x,y,w] ) by A56; :: thesis: verum
end;
consider Smn being Function of [:(Seg (len (T . n))),(Seg (len (T . m))):], the carrier of X such that
A57: for x, y being object st x in Seg (len (T . n)) & y in Seg (len (T . m)) holds
S5[x,y,Smn . (x,y)] from BINOP_1:sch 1(A54);
A58: for i, j being Nat st i in Seg (len (T . n)) & j in Seg (len (T . m)) holds
ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
proof
let i, j be Nat; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) )
assume ( i in Seg (len (T . n)) & j in Seg (len (T . m)) ) ; :: thesis: ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z )
then ex i1, j1 being Nat ex z being Point of X st
( i = i1 & j = j1 & z = (h | (divset ((T . m),j1))) . (p2 . j1) & Smn . (i,j) = (xvol ((divset ((T . n),i1)) /\ (divset ((T . m),j1)))) * z ) by A57;
hence ex z being Point of X st
( z = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z ) ; :: thesis: verum
end;
defpred S6[ Nat, object ] means ex s being FinSequence of X st
( dom s = Seg (len (T . n)) & $2 = Sum s & ( for i being Nat st i in dom s holds
s . i = Smn . (i,$1) ) );
A59: for k being Nat st k in Seg (len (T . m)) holds
ex x being object st S6[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len (T . m)) implies ex x being object st S6[k,x] )
assume A60: k in Seg (len (T . m)) ; :: thesis: ex x being object st S6[k,x]
deffunc H1( set ) -> set = Smn . ($1,k);
consider s being FinSequence such that
A61: len s = len (T . n) and
A62: for i being Nat st i in dom s holds
s . i = H1(i) from FINSEQ_1:sch 2();
 A63: dom s = Seg (len (T . n)) by A61, FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in the carrier of X
proof
let i be Nat; :: thesis: ( i in dom s implies s . i in the carrier of X )
assume A64: i in dom s ; :: thesis: s . i in the carrier of X
then [i,k] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A63, A60, ZFMISC_1:87;
then Smn . (i,k) in the carrier of X by FUNCT_2:5;
hence s . i in the carrier of X by A62, A64; :: thesis: verum
end;
then reconsider s = s as FinSequence of X by FINSEQ_2:12;
take x = Sum s; :: thesis: S6[k,x]
thus S6[k,x] by A62, A63; :: thesis: verum
end;
consider Zq being FinSequence such that
A65: ( dom Zq = Seg (len (T . m)) & ( for k being Nat st k in Seg (len (T . m)) holds
S6[k,Zq . k] ) ) from FINSEQ_1:sch 1(A59);
 for j being Nat st j in dom Zq holds
Zq . j in the carrier of X
proof
let j be Nat; :: thesis: ( j in dom Zq implies Zq . j in the carrier of X )
assume j in dom Zq ; :: thesis: Zq . j in the carrier of X
then ex s being FinSequence of X st
( dom s = Seg (len (T . n)) & Zq . j = Sum s & ( for i being Nat st i in dom s holds
s . i = Smn . (i,j) ) ) by A65;
hence Zq . j in the carrier of X ; :: thesis: verum
end;
then reconsider Zq = Zq as FinSequence of X by FINSEQ_2:12;
A66: len Zq = len (T . m) by FINSEQ_1:def 3, A65;
for k being Nat st 1 <= k & k <= len Zq holds
Zq . k = (S . m) . k
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len Zq implies Zq . k = (S . m) . k )
assume A67: ( 1 <= k & k <= len Zq ) ; :: thesis: Zq . k = (S . m) . k
then consider s being FinSequence of X such that
A68: ( dom s = Seg (len (T . n)) & Zq . k = Sum s & ( for i being Nat st i in dom s holds
s . i = Smn . (i,k) ) ) by A65, FINSEQ_3:25;
A69: k in Seg (len (T . m)) by A67, A66;
A70: k in dom (T . m) by A67, A66, FINSEQ_3:25;
then consider z being Point of X such that
A71: ( z = (h | (divset ((T . m),k))) . (p2 . k) & (S . m) . k = (vol (divset ((T . m),k))) * z ) by A21;
defpred S7[ Nat, set ] means $2 = xvol ((divset ((T . n),$1)) /\ (divset ((T . m),k)));
A72: for i being Nat st i in Seg (len s) holds
ex x being Element of REAL st S7[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len s) implies ex x being Element of REAL st S7[i,x] )
assume i in Seg (len s) ; :: thesis: ex x being Element of REAL st S7[i,x]
xvol ((divset ((T . n),i)) /\ (divset ((T . m),k))) in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S7[i,x] ; :: thesis: verum
end;
consider vtntm being FinSequence of REAL such that
A73: ( dom vtntm = Seg (len s) & ( for i being Nat st i in Seg (len s) holds
S7[i,vtntm . i] ) ) from FINSEQ_1:sch 5(A72);
 A74: ( dom vtntm = dom s & len vtntm = len s ) by A73, FINSEQ_1:def 3;
A75: for j being Nat st j in dom vtntm holds
vtntm . j = xvol ((divset ((T . m),k)) /\ (divset ((T . n),j))) by A73;
len s = len (T . n) by A68, FINSEQ_1:def 3;
then A76: Sum vtntm = vol (divset ((T . m),k)) by Th8, A75, A74, A70, INTEGRA1:8;
for j being Nat st j in dom s holds
ex x being Real st
( x = vtntm . j & s . j = x * z )
proof
let j be Nat; :: thesis: ( j in dom s implies ex x being Real st
( x = vtntm . j & s . j = x * z ) )
assume A77: j in dom s ; :: thesis: ex x being Real st
( x = vtntm . j & s . j = x * z )
then A78: ex w being Point of X st
( w = (h | (divset ((T . m),k))) . (p2 . k) & Smn . (j,k) = (xvol ((divset ((T . n),j)) /\ (divset ((T . m),k)))) * w ) by A58, A69, A68;
take vtntm . j ; :: thesis: ( vtntm . j = vtntm . j & s . j = (vtntm . j) * z )
s . j = (xvol ((divset ((T . n),j)) /\ (divset ((T . m),k)))) * z by A71, A78, A77, A68;
hence ( vtntm . j = vtntm . j & s . j = (vtntm . j) * z ) by A77, A73, A74; :: thesis: verum
end;
hence Zq . k = (S . m) . k by A71, A68, A76, Th7, A74; :: thesis: verum
end;
then Zq = S . m by INTEGR18:def 1, A66;
then A79: (Sum (S . n)) - (Sum (S . m)) = (Sum Xq) - (Sum Zq) by Th4, A33, A53, A46;
set XZq = Xq - Zq;
A80: dom (Xq - Zq) = (dom Xq) /\ (dom Zq) by VFUNCT_1:def 2;
then reconsider XZq = Xq - Zq as FinSequence by A53, A65, FINSEQ_1:def 2;
now :: thesis: for i being Nat st i in dom XZq holds
XZq . i in the carrier of X
let i be Nat; :: thesis: ( i in dom XZq implies XZq . i in the carrier of X )
assume i in dom XZq ; :: thesis: XZq . i in the carrier of X
then XZq . i = (Xq - Zq) /. i by PARTFUN1:def 6;
hence XZq . i in the carrier of X ; :: thesis: verum
end;
then reconsider XZq = Xq - Zq as FinSequence of X by FINSEQ_2:12;
len Xq = len Zq by FINSEQ_3:29, A53, A65;
then A81: (Sum (S . n)) - (Sum (S . m)) = Sum XZq by A79, INTEGR18:2;
A82: for i, j being Nat
for Snmij, Smnij being Point of X st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
proof
let i, j be Nat; :: thesis: for Snmij, Smnij being Point of X st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
let Snmij, Smnij be Point of X; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) implies ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1)) )
assume A83: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) ) ; :: thesis: ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
then consider z1 being Point of X such that
A84: ( z1 = (h | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z1 ) by A26;
consider z2 being Point of X such that
A85: ( z2 = (h | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * z2 ) by A58, A83;
A86: ( i in dom (T . n) & j in dom (T . m) ) by A83, FINSEQ_1:def 3;
then A87: ( p1 . i in dom (h | (divset ((T . n),i))) & p2 . j in dom (h | (divset ((T . m),j))) ) by A20, A21;
then ( p1 . i in (dom h) /\ (divset ((T . n),i)) & p2 . j in (dom h) /\ (divset ((T . m),j)) ) by RELAT_1:61;
then A88: ( p1 . i in dom h & p1 . i in divset ((T . n),i) & p2 . j in dom h & p2 . j in divset ((T . m),j) ) by XBOOLE_0:def 4;
( z1 = h . (p1 . i) & z2 = h . (p2 . j) ) by A84, A85, A87, FUNCT_1:47;
then A89: ( z1 = h /. (p1 . i) & z2 = h /. (p2 . j) ) by A88, PARTFUN1:def 6;
per cases ( (divset ((T . n),i)) /\ (divset ((T . m),j)) = {} or (divset ((T . n),i)) /\ (divset ((T . m),j)) <> {} ) ;
suppose A90: (divset ((T . n),i)) /\ (divset ((T . m),j)) = {} ; :: thesis: ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
then A91: xvol ((divset ((T . n),i)) /\ (divset ((T . m),j))) = 0 by Def2;
( Snmij = 0. X & Smnij = 0. X ) by A83, A84, A85, A90, Def2, RLVECT_1:10;
hence ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1)) by A91; :: thesis: verum
end;
suppose (divset ((T . n),i)) /\ (divset ((T . m),j)) <> {} ; :: thesis: ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1))
then consider t being object such that
A92: t in (divset ((T . n),i)) /\ (divset ((T . m),j)) by XBOOLE_0:def 1;
reconsider t = t as Real by A92;
A93: dom h = A by FUNCT_2:def 1;
A94: divset ((T . m),j) c= A by A86, INTEGRA1:8;
A95: ( t in divset ((T . n),i) & t in divset ((T . m),j) ) by A92, XBOOLE_0:def 4;
then ( |.((p1 . i) - t).| < sk & |.(t - (p2 . j)).| < sk ) by A86, A88, Th12, A18;
then A96: ( ||.((h /. (p1 . i)) - (h /. t)).|| < ((p / 2) / ((vol A) + 1)) / 2 & ||.((h /. t) - (h /. (p2 . j))).|| < ((p / 2) / ((vol A) + 1)) / 2 ) by A94, A95, A93, A88, A15;
reconsider DMN = (divset ((T . n),i)) /\ (divset ((T . m),j)) as real-bounded Subset of REAL by XBOOLE_1:17, XXREAL_2:45;
Snmij - Smnij = (xvol DMN) * (((h /. (p1 . i)) - (0. X)) - (h /. (p2 . j))) by A83, A84, A89, A85, RLVECT_1:34;
then Snmij - Smnij = (xvol DMN) * (((h /. (p1 . i)) - ((h /. t) - (h /. t))) - (h /. (p2 . j))) by RLVECT_1:15;
then Snmij - Smnij = (xvol DMN) * ((((h /. (p1 . i)) - (h /. t)) + (h /. t)) - (h /. (p2 . j))) by RLVECT_1:29;
then Snmij - Smnij = (xvol DMN) * (((h /. (p1 . i)) - (h /. t)) + ((h /. t) - (h /. (p2 . j)))) by RLVECT_1:28;
then Snmij - Smnij = ((xvol DMN) * ((h /. (p1 . i)) - (h /. t))) + ((xvol DMN) * ((h /. t) - (h /. (p2 . j)))) by RLVECT_1:def 5;
then A97: ||.(Snmij - Smnij).|| <= ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| by NORMSP_1:def 1;
( ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = |.(xvol DMN).| * ||.((h /. (p1 . i)) - (h /. t)).|| & ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = |.(xvol DMN).| * ||.((h /. t) - (h /. (p2 . j))).|| ) by NORMSP_1:def 1;
then A98: ( ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| = (xvol DMN) * ||.((h /. (p1 . i)) - (h /. t)).|| & ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| = (xvol DMN) * ||.((h /. t) - (h /. (p2 . j))).|| ) by Th5, ABSVALUE:def 1;
0 <= xvol DMN by Th5;
then ( ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| <= (xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2) & ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| <= (xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2) ) by A98, A96, XREAL_1:64;
then ||.((xvol DMN) * ((h /. (p1 . i)) - (h /. t))).|| + ||.((xvol DMN) * ((h /. t) - (h /. (p2 . j)))).|| <= ((xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2)) + ((xvol DMN) * (((p / 2) / ((vol A) + 1)) / 2)) by XREAL_1:7;
hence ||.(Snmij - Smnij).|| <= (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) * ((p / 2) / ((vol A) + 1)) by A97, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A99: for j being Nat st j in dom XZq holds
||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
proof
let j be Nat; :: thesis: ( j in dom XZq implies ||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1)) )
assume A100: j in dom XZq ; :: thesis: ||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1))
then A101: XZq /. j = (Xq /. j) - (Zq /. j) by VFUNCT_1:def 2;
A102: ( Xq /. j = Xq . j & Zq /. j = Zq . j ) by A100, A65, A53, A80, PARTFUN1:def 6;
A103: dom XZq = (dom Xq) /\ (dom Zq) by VFUNCT_1:def 2;
consider Xsq being FinSequence of X such that
A104: ( dom Xsq = Seg (len (T . n)) & Xq . j = Sum Xsq & ( for i being Nat st i in dom Xsq holds
Xsq . i = Snm . (i,j) ) ) by A100, A53, A65, A80;
consider Zsq being FinSequence of X such that
A105: ( dom Zsq = Seg (len (T . n)) & Zq . j = Sum Zsq & ( for i being Nat st i in dom Zsq holds
Zsq . i = Smn . (i,j) ) ) by A100, A65, A53, A80;
set XZsq = Xsq - Zsq;
A106: dom (Xsq - Zsq) = (dom Xsq) /\ (dom Zsq) by VFUNCT_1:def 2;
then reconsider XZsq = Xsq - Zsq as FinSequence by A104, A105, FINSEQ_1:def 2;
now :: thesis: for i being Nat st i in dom XZsq holds
XZsq . i in the carrier of X
let i be Nat; :: thesis: ( i in dom XZsq implies XZsq . i in the carrier of X )
assume i in dom XZsq ; :: thesis: XZsq . i in the carrier of X
then XZsq . i = (Xsq - Zsq) /. i by PARTFUN1:def 6;
hence XZsq . i in the carrier of X ; :: thesis: verum
end;
then reconsider XZsq = XZsq as FinSequence of X by FINSEQ_2:12;
defpred S7[ Nat, set ] means $2 = xvol ((divset ((T . n),$1)) /\ (divset ((T . m),j)));
A107: for i being Nat st i in Seg (len XZsq) holds
ex x being Element of REAL st S7[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len XZsq) implies ex x being Element of REAL st S7[i,x] )
assume i in Seg (len XZsq) ; :: thesis: ex x being Element of REAL st S7[i,x]
xvol ((divset ((T . n),i)) /\ (divset ((T . m),j))) in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S7[i,x] ; :: thesis: verum
end;
consider vtntm being FinSequence of REAL such that
A108: ( dom vtntm = Seg (len XZsq) & ( for i being Nat st i in Seg (len XZsq) holds
S7[i,vtntm . i] ) ) from FINSEQ_1:sch 5(A107);
 A109: for i being Nat st i in dom vtntm holds
vtntm . i = xvol ((divset ((T . m),j)) /\ (divset ((T . n),i))) by A108;
A110: len vtntm = len XZsq by A108, FINSEQ_1:def 3;
A111: len XZsq = len (T . n) by A104, A105, A106, FINSEQ_1:def 3;
reconsider pvtntm = ((p / 2) / ((vol A) + 1)) * vtntm as FinSequence of REAL ;
j in dom (T . m) by A100, A103, A53, A65, FINSEQ_1:def 3;
then divset ((T . m),j) c= A by INTEGRA1:8;
then Sum vtntm = vol (divset ((T . m),j)) by Th8, A109, A110, A104, A105, A106, FINSEQ_1:def 3;
then A112: Sum pvtntm = ((p / 2) / ((vol A) + 1)) * (vol (divset ((T . m),j))) by RVSUM_1:87;
dom pvtntm = dom vtntm by VALUED_1:def 5;
then dom pvtntm = Seg (len (T . n)) by A104, A105, A106, A108, FINSEQ_1:def 3;
then A113: len pvtntm = len (T . n) by FINSEQ_1:def 3;
for i being Nat st i in dom XZsq holds
||.(XZsq /. i).|| <= pvtntm . i
proof
let i be Nat; :: thesis: ( i in dom XZsq implies ||.(XZsq /. i).|| <= pvtntm . i )
assume A114: i in dom XZsq ; :: thesis: ||.(XZsq /. i).|| <= pvtntm . i
then A115: XZsq /. i = (Xsq /. i) - (Zsq /. i) by VFUNCT_1:def 2;
( Xsq /. i = Xsq . i & Zsq /. i = Zsq . i ) by PARTFUN1:def 6, A114, A105, A106, A104;
then A116: ( Xsq /. i = Snm . (i,j) & Zsq /. i = Smn . (i,j) ) by A114, A104, A106, A105;
dom vtntm = dom XZsq by A108, FINSEQ_1:def 3;
then ((p / 2) / ((vol A) + 1)) * (vtntm . i) = ((p / 2) / ((vol A) + 1)) * (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) by A108, A114;
then (((p / 2) / ((vol A) + 1)) (#) vtntm) . i = ((p / 2) / ((vol A) + 1)) * (xvol ((divset ((T . n),i)) /\ (divset ((T . m),j)))) by VALUED_1:6;
hence ||.(XZsq /. i).|| <= pvtntm . i by A115, A116, A82, A114, A104, A105, A106, A100, A103, A53, A65; :: thesis: verum
end;
then A117: ||.(Sum XZsq).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1)) by A112, Th10, A111, A113;
len Xsq = len Zsq by FINSEQ_3:29, A104, A105;
hence ||.(XZq /. j).|| <= (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1)) by A101, A102, A104, A105, A117, INTEGR18:2; :: thesis: verum
end;
defpred S7[ Nat, set ] means $2 = vol (divset ((T . m),$1));
A118: for i being Nat st i in Seg (len XZq) holds
ex x being Element of REAL st S7[i,x]
proof
let i be Nat; :: thesis: ( i in Seg (len XZq) implies ex x being Element of REAL st S7[i,x] )
assume i in Seg (len XZq) ; :: thesis: ex x being Element of REAL st S7[i,x]
vol (divset ((T . m),i)) in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S7[i,x] ; :: thesis: verum
end;
consider vtm being FinSequence of REAL such that
A119: ( dom vtm = Seg (len XZq) & ( for i being Nat st i in Seg (len XZq) holds
S7[i,vtm . i] ) ) from FINSEQ_1:sch 5(A118);
A120: len XZq = len (T . m) by A53, A65, A80, FINSEQ_1:def 3;
A121: Seg (len XZq) = dom XZq by FINSEQ_1:def 3;
A122: Sum vtm = vol A by A119, Th6, A120;
reconsider pvtm = ((p / 2) / ((vol A) + 1)) * vtm as FinSequence of REAL ;
dom pvtm = dom vtm by VALUED_1:def 5;
then dom pvtm = Seg (len (T . m)) by A53, A65, A80, A119, FINSEQ_1:def 3;
then A123: len pvtm = len (T . m) by FINSEQ_1:def 3;
A124: Sum pvtm = ((p / 2) / ((vol A) + 1)) * (vol A) by RVSUM_1:87, A122;
for j being Nat st j in dom XZq holds
||.(XZq /. j).|| <= pvtm . j
proof
let j be Nat; :: thesis: ( j in dom XZq implies ||.(XZq /. j).|| <= pvtm . j )
assume A125: j in dom XZq ; :: thesis: ||.(XZq /. j).|| <= pvtm . j
then vtm . j = vol (divset ((T . m),j)) by A119, A121;
then pvtm . j = (vol (divset ((T . m),j))) * ((p / 2) / ((vol A) + 1)) by VALUED_1:6;
hence ||.(XZq /. j).|| <= pvtm . j by A125, A99; :: thesis: verum
end;
then ||.(Sum XZq).|| <= (vol A) * ((p / 2) / ((vol A) + 1)) by A124, A120, A123, Th10;
hence ||.(((middle_sum (h,S)) . n) - ((middle_sum (h,S)) . m)).|| < p by A19, A81, XXREAL_0:2, A14; :: thesis: verum
end;
hence middle_sum (h,S) is convergent by RSSPACE3:8, LOPBAN_1:def 15; :: thesis: verum
end;