let A be non empty closed_interval Subset of REAL; :: thesis: for rho being Function of A,REAL
for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
let rho be Function of A,REAL; :: thesis: for u being PartFunc of REAL,REAL st rho is bounded_variation & dom u = A & u | A is uniformly_continuous holds
for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
let u be PartFunc of REAL,REAL; :: thesis: ( rho is bounded_variation & dom u = A & u | A is uniformly_continuous implies for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent )
assume that
A1: ( rho is bounded_variation & dom u = A ) and
A2: u | A is uniformly_continuous ; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
thus for T being DivSequence of A
for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent :: thesis: verum
proof
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of rho,u,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum S is convergent
let S be middle_volume_Sequence of rho,u,T; :: thesis: ( delta T is convergent & lim (delta T) = 0 implies middle_sum S is convergent )
assume A4: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: middle_sum 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 (u | (divset ((T . $1),i))) & ex z being Real st
( z = (u | (divset ((T . $1),i))) . (p . i) & (S . $1) . i = z * (vol ((divset ((T . $1),i)),rho)) ) ) ) );
A5: 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 (u | (divset ((T . k),$1))) & ex c being Real st
( c = (u | (divset ((T . k),$1))) . $2 & (S . k) . $1 = c * (vol ((divset ((T . k),$1)),rho)) ) );
A6: Seg (len (T . k)) = dom (T . k) by FINSEQ_1:def 3;
A7: 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 Real such that
A8: ( c in rng (u | (divset ((T . k),i))) & (S . k) . i = c * (vol ((divset ((T . k),i)),rho)) ) by A1, INTEGR22:def 5;
consider x being object such that
A9: ( x in dom (u | (divset ((T . k),i))) & c = (u | (divset ((T . k),i))) . x ) by A8, FUNCT_1:def 3;
reconsider x = x as Element of REAL by A9;
take x ; :: thesis: S2[i,x]
thus S2[i,x] by A8, A9; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A10: ( 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(A7);
 take p ; :: thesis: ( p is Element of REAL * & S1[k,p] )
len p = len (T . k) by A10, FINSEQ_1:def 3;
hence ( p is Element of REAL * & S1[k,p] ) by A6, A10, FINSEQ_1:def 11; :: thesis: verum
end;
consider Fn being sequence of (REAL *) such that
A11: for x being Element of NAT holds S1[x,Fn . x] from FUNCT_2:sch 3(A5);
 consider Fm being sequence of (REAL *) such that
A12: for x being Element of NAT holds S1[x,Fm . x] from FUNCT_2:sch 3(A5);
 set TVD = total_vd rho;
A13: 0 <= total_vd rho by A1, INTEGR22:6;
now :: thesis: for p being Real st p > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p
let p be Real; :: thesis: ( p > 0 implies ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p )
set pp2 = p / 2;
set pv = (p / 2) / ((total_vd rho) + 1);
assume B13: p > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p
then A14: ( 0 < p / 2 & p / 2 < p ) by XREAL_1:215, XREAL_1:216;
then A15: 0 < (p / 2) / ((total_vd rho) + 1) by A13, XREAL_1:139;
then ((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < ((p / 2) / ((total_vd rho) + 1)) * ((total_vd rho) + 1) by XREAL_1:29, XREAL_1:68;
then ((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < p / 2 by A13, XCMPLX_1:87;
then A16: ((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) < p by A14, XXREAL_0:2;
set p2v = ((p / 2) / ((total_vd rho) + 1)) / 2;
consider sk being Real such that
A17: ( 0 < sk & ( for x1, x2 being Real st x1 in dom (u | A) & x2 in dom (u | A) & |.(x1 - x2).| < sk holds
|.(((u | A) . x1) - ((u | A) . x2)).| < ((p / 2) / ((total_vd rho) + 1)) / 2 ) ) by A2, A15, FCONT_2:def 1, XREAL_1:215;
consider m being Nat such that
A18: for i being Nat st m <= i holds
|.(((delta T) . i) - 0).| < sk by A4, A17, SEQ_2:def 7;
take m = m; :: thesis: for n being Nat st n >= m holds
|.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p
let n be Nat; :: thesis: ( n >= m implies |.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p )
A19: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
assume n >= m ; :: thesis: |.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p
then ( |.(((delta T) . n) - 0).| < sk & |.(((delta T) . m) - 0).| < sk ) by A18;
then ( |.(delta (T . n)).| < sk & |.(delta (T . m)).| < sk ) by A19, INTEGRA3:def 2;
then A20: ( delta (T . n) < sk & delta (T . m) < sk ) by ABSVALUE:def 1, INTEGRA3:9;
A21: ( (middle_sum S) . n = Sum (S . n) & (middle_sum S) . m = Sum (S . m) ) by INTEGR22:def 7;
consider p1 being FinSequence of REAL such that
A22: ( p1 = Fn . n & len p1 = len (T . n) & ( for i being Nat st i in dom (T . n) holds
( p1 . i in dom (u | (divset ((T . n),i))) & ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & (S . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) ) ) ) by A11, A19;
consider p2 being FinSequence of REAL such that
A23: ( p2 = Fm . m & len p2 = len (T . m) & ( for i being Nat st i in dom (T . m) holds
( p2 . i in dom (u | (divset ((T . m),i))) & ex z being Real st
( z = (u | (divset ((T . m),i))) . (p2 . i) & (S . m) . i = z * (vol ((divset ((T . m),i)),rho)) ) ) ) ) by A12, A19;
defpred S2[ object , object , object ] means ex i, j being Nat ex z being Real st
( $1 = i & $2 = j & z = (u | (divset ((T . n),i))) . (p1 . i) & $3 = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z );
A24: 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 REAL & 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 REAL & S2[x,y,w] ) )
assume A25: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) ) ; :: thesis: ex w being object st
( w in REAL & S2[x,y,w] )
then reconsider i = x, j = y as Nat ;
i in dom (T . n) by A25, FINSEQ_1:def 3;
then consider z being Real such that
A26: ( z = (u | (divset ((T . n),i))) . (p1 . i) & (S . n) . i = z * (vol ((divset ((T . n),i)),rho)) ) by A22;
(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z in REAL by XREAL_0:def 1;
hence ex w being object st
( w in REAL & S2[x,y,w] ) by A26; :: thesis: verum
end;
consider Snm being Function of [:(Seg (len (T . n))),(Seg (len (T . m))):],REAL such that
A27: 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(A24);
A28: for i, j being Nat st i in Seg (len (T . n)) & j in Seg (len (T . m)) holds
ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
proof
let i, j be Nat; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) )
assume ( i in Seg (len (T . n)) & j in Seg (len (T . m)) ) ; :: thesis: ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
then ex i1, j1 being Nat ex z being Real st
( i = i1 & j = j1 & z = (u | (divset ((T . n),i1))) . (p1 . i1) & Snm . (i,j) = (vol (((divset ((T . n),i1)) /\ (divset ((T . m),j1))),rho)) * z ) by A27;
hence ex z being Real st
( z = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) ; :: thesis: verum
end;
defpred S3[ Nat, object ] means ex r being FinSequence of REAL 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) ) );
A29: 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 A30: 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
A31: len r = len (T . m) and
A32: for j being Nat st j in dom r holds
r . j = H1(j) from FINSEQ_1:sch 2();
 A33: dom r = Seg (len (T . m)) by A31, FINSEQ_1:def 3;
for j being Nat st j in dom r holds
r . j in REAL
proof
let j be Nat; :: thesis: ( j in dom r implies r . j in REAL )
assume A34: j in dom r ; :: thesis: r . j in REAL
then [k,j] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A30, A33, ZFMISC_1:87;
then Snm . (k,j) in REAL by FUNCT_2:5;
hence r . j in REAL by A32, A34; :: thesis: verum
end;
then reconsider r = r as FinSequence of REAL by FINSEQ_2:12;
take x = Sum r; :: thesis: S3[k,x]
thus S3[k,x] by A32, A33; :: thesis: verum
end;
consider Xp being FinSequence such that
A35: ( 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(A29);
 for i being Nat st i in dom Xp holds
Xp . i in REAL
proof
let i be Nat; :: thesis: ( i in dom Xp implies Xp . i in REAL )
assume i in dom Xp ; :: thesis: Xp . i in REAL
then ex r being FinSequence of REAL 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 A35;
hence Xp . i in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider Xp = Xp as FinSequence of REAL by FINSEQ_2:12;
A36: len Xp = len (T . n) by A35, FINSEQ_1:def 3;
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 A38: ( k in Seg (len Xp) & k in Seg (len (T . n)) ) by A36;
then A39: ( k in dom Xp & k in dom (T . n) ) by FINSEQ_1:def 3;
then consider z being Real such that
A40: ( z = (u | (divset ((T . n),k))) . (p1 . k) & (S . n) . k = z * (vol ((divset ((T . n),k)),rho)) ) by A22;
consider r being FinSequence of REAL such that
A41: ( 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, A38;
defpred S4[ Nat, set ] means $2 = vol (((divset ((T . n),k)) /\ (divset ((T . m),$1))),rho);
A42: 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]
vol (((divset ((T . n),k)) /\ (divset ((T . m),i))),rho) 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
A43: ( 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(A42);
 A44: ( dom vtntm = dom r & ( for j being Nat st j in dom vtntm holds
vtntm . j = vol (((divset ((T . n),k)) /\ (divset ((T . m),j))),rho) ) ) by A43, FINSEQ_1:def 3;
A45: ( len vtntm = len r & len (T . m) = len r ) by A41, A43, FINSEQ_1:def 3;
then A46: Sum vtntm = vol ((divset ((T . n),k)),rho) by A39, A43, INTEGR22:1, 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 A47: j in dom r ; :: thesis: ex x being Real st
( x = vtntm . j & r . j = x * z )
then A48: ex w being Real st
( w = (u | (divset ((T . n),k))) . (p1 . k) & Snm . (k,j) = (vol (((divset ((T . n),k)) /\ (divset ((T . m),j))),rho)) * w ) by A28, A38, A41;
take vtntm . j ; :: thesis: ( vtntm . j = vtntm . j & r . j = (vtntm . j) * z )
r . j = (vol (((divset ((T . n),k)) /\ (divset ((T . m),j))),rho)) * z by A40, A41, A47, A48;
hence ( vtntm . j = vtntm . j & r . j = (vtntm . j) * z ) by A44, A47; :: thesis: verum
end;
hence Xp . k = (S . n) . k by A40, A41, A45, A46, Th1; :: thesis: verum
end;
then A49: Xp = S . n by A1, A36, INTEGR22:def 5;
defpred S4[ Nat, object ] means ex s being FinSequence of REAL 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) ) );
A50: 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 A51: 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
A52: len s = len (T . n) and
A53: for i being Nat st i in dom s holds
s . i = H1(i) from FINSEQ_1:sch 2();
 A54: dom s = Seg (len (T . n)) by A52, FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in REAL
proof
let i be Nat; :: thesis: ( i in dom s implies s . i in REAL )
assume A55: i in dom s ; :: thesis: s . i in REAL
then [i,k] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A51, A54, ZFMISC_1:87;
then Snm . (i,k) in REAL by FUNCT_2:5;
hence s . i in REAL by A53, A55; :: thesis: verum
end;
then reconsider s = s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s; :: thesis: S4[k,x]
thus S4[k,x] by A53, A54; :: thesis: verum
end;
consider Xq being FinSequence such that
A56: ( 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(A50);
 for j being Nat st j in dom Xq holds
Xq . j in REAL
proof
let j be Nat; :: thesis: ( j in dom Xq implies Xq . j in REAL )
assume j in dom Xq ; :: thesis: Xq . j in REAL
then ex s being FinSequence of REAL 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 A56;
hence Xq . j in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider Xq = Xq as FinSequence of REAL by FINSEQ_2:12;
defpred S5[ object , object , object ] means ex i, j being Nat ex z being Real st
( $1 = i & $2 = j & z = (u | (divset ((T . m),j))) . (p2 . j) & $3 = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z );
A57: 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 REAL & 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 REAL & S5[x,y,w] ) )
assume A58: ( x in Seg (len (T . n)) & y in Seg (len (T . m)) ) ; :: thesis: ex w being object st
( w in REAL & S5[x,y,w] )
then reconsider i = x, j = y as Nat ;
j in dom (T . m) by A58, FINSEQ_1:def 3;
then consider z being Real such that
A59: ( z = (u | (divset ((T . m),j))) . (p2 . j) & (S . m) . j = z * (vol ((divset ((T . m),j)),rho)) ) by A23;
(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z in REAL by XREAL_0:def 1;
hence ex w being object st
( w in REAL & S5[x,y,w] ) by A59; :: thesis: verum
end;
consider Smn being Function of [:(Seg (len (T . n))),(Seg (len (T . m))):],REAL such that
A60: 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(A57);
A61: for i, j being Nat st i in Seg (len (T . n)) & j in Seg (len (T . m)) holds
ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
proof
let i, j be Nat; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) implies ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) )
assume ( i in Seg (len (T . n)) & j in Seg (len (T . m)) ) ; :: thesis: ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z )
then ex i1, j1 being Nat ex z being Real st
( i = i1 & j = j1 & z = (u | (divset ((T . m),j1))) . (p2 . j1) & Smn . (i,j) = (vol (((divset ((T . n),i1)) /\ (divset ((T . m),j1))),rho)) * z ) by A60;
hence ex z being Real st
( z = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z ) ; :: thesis: verum
end;
defpred S6[ Nat, object ] means ex s being FinSequence of REAL 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) ) );
A62: 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 A63: 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
A64: len s = len (T . n) and
A65: for i being Nat st i in dom s holds
s . i = H1(i) from FINSEQ_1:sch 2();
 A66: dom s = Seg (len (T . n)) by A64, FINSEQ_1:def 3;
for i being Nat st i in dom s holds
s . i in REAL
proof
let i be Nat; :: thesis: ( i in dom s implies s . i in REAL )
assume A67: i in dom s ; :: thesis: s . i in REAL
then [i,k] in [:(Seg (len (T . n))),(Seg (len (T . m))):] by A63, A66, ZFMISC_1:87;
then Smn . (i,k) in REAL by FUNCT_2:5;
hence s . i in REAL by A65, A67; :: thesis: verum
end;
then reconsider s = s as FinSequence of REAL by FINSEQ_2:12;
take x = Sum s; :: thesis: S6[k,x]
thus S6[k,x] by A65, A66; :: thesis: verum
end;
consider Zq being FinSequence such that
A68: ( 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(A62);
 for j being Nat st j in dom Zq holds
Zq . j in REAL
proof
let j be Nat; :: thesis: ( j in dom Zq implies Zq . j in REAL )
assume j in dom Zq ; :: thesis: Zq . j in REAL
then ex s being FinSequence of REAL 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 A68;
hence Zq . j in REAL by XREAL_0:def 1; :: thesis: verum
end;
then reconsider Zq = Zq as FinSequence of REAL by FINSEQ_2:12;
A69: len Zq = len (T . m) by A68, FINSEQ_1:def 3;
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 A71: ( 1 <= k & k <= len Zq ) ; :: thesis: Zq . k = (S . m) . k
then consider s being FinSequence of REAL such that
A72: ( 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 A68, FINSEQ_3:25;
A73: k in Seg (len (T . m)) by A69, A71;
A74: k in dom (T . m) by A69, A71, FINSEQ_3:25;
then consider z being Real such that
A75: ( z = (u | (divset ((T . m),k))) . (p2 . k) & (S . m) . k = z * (vol ((divset ((T . m),k)),rho)) ) by A23;
defpred S7[ Nat, set ] means $2 = vol (((divset ((T . n),$1)) /\ (divset ((T . m),k))),rho);
A76: 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]
vol (((divset ((T . n),i)) /\ (divset ((T . m),k))),rho) 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
A77: ( 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(A76);
 A78: ( dom vtntm = dom s & len vtntm = len s ) by A77, FINSEQ_1:def 3;
A79: for j being Nat st j in dom vtntm holds
vtntm . j = vol (((divset ((T . m),k)) /\ (divset ((T . n),j))),rho) by A77;
len s = len (T . n) by A72, FINSEQ_1:def 3;
then A80: Sum vtntm = vol ((divset ((T . m),k)),rho) by A74, A78, A79, INTEGR22:1, 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 A81: j in dom s ; :: thesis: ex x being Real st
( x = vtntm . j & s . j = x * z )
then A82: ex w being Real st
( w = (u | (divset ((T . m),k))) . (p2 . k) & Smn . (j,k) = (vol (((divset ((T . n),j)) /\ (divset ((T . m),k))),rho)) * w ) by A61, A72, A73;
take vtntm . j ; :: thesis: ( vtntm . j = vtntm . j & s . j = (vtntm . j) * z )
s . j = (vol (((divset ((T . n),j)) /\ (divset ((T . m),k))),rho)) * z by A72, A75, A81, A82;
hence ( vtntm . j = vtntm . j & s . j = (vtntm . j) * z ) by A77, A78, A81; :: thesis: verum
end;
hence Zq . k = (S . m) . k by A72, A75, A78, A80, Th1; :: thesis: verum
end;
then Zq = S . m by A1, A69, INTEGR22:def 5;
then A83: (Sum (S . n)) - (Sum (S . m)) = (Sum Xq) - (Sum Zq) by A35, A49, A56, INTEGR22:2;
set XZq = Xq - Zq;
A84: dom (Xq - Zq) = (dom Xq) /\ (dom Zq) by VALUED_1:12;
reconsider XZq = Xq - Zq as FinSequence of REAL ;
len Xq = len Zq by A56, A68, FINSEQ_3:29;
then A86: ( Xq is Element of (len Xq) -tuples_on REAL & Zq is Element of (len Xq) -tuples_on REAL ) by FINSEQ_2:92;
A87: for i, j being Nat
for Snmij, Smnij being Real st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
proof
let i, j be Nat; :: thesis: for Snmij, Smnij being Real st i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) holds
|.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
let Snmij, Smnij be Real; :: thesis: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) implies |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1)) )
assume A88: ( i in Seg (len (T . n)) & j in Seg (len (T . m)) & Snmij = Snm . (i,j) & Smnij = Smn . (i,j) ) ; :: thesis: |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
then consider z1 being Real such that
A89: ( z1 = (u | (divset ((T . n),i))) . (p1 . i) & Snm . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z1 ) by A28;
consider z2 being Real such that
A90: ( z2 = (u | (divset ((T . m),j))) . (p2 . j) & Smn . (i,j) = (vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)) * z2 ) by A61, A88;
A91: ( i in dom (T . n) & j in dom (T . m) ) by A88, FINSEQ_1:def 3;
then A92: ( p1 . i in dom (u | (divset ((T . n),i))) & p2 . j in dom (u | (divset ((T . m),j))) ) by A22, A23;
then ( p1 . i in (dom u) /\ (divset ((T . n),i)) & p2 . j in (dom u) /\ (divset ((T . m),j)) ) by RELAT_1:61;
then A93: ( p1 . i in dom u & p1 . i in divset ((T . n),i) & p2 . j in dom u & p2 . j in divset ((T . m),j) ) by XBOOLE_0:def 4;
A94: ( z1 = u . (p1 . i) & z2 = u . (p2 . j) ) by A89, A90, A92, FUNCT_1:47;
per cases ( (divset ((T . n),i)) /\ (divset ((T . m),j)) = {} or (divset ((T . n),i)) /\ (divset ((T . m),j)) <> {} ) ;
suppose (divset ((T . n),i)) /\ (divset ((T . m),j)) = {} ; :: thesis: |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
then vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho) = 0 by INTEGR22:def 1;
hence |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1)) by A88, A89, A90, COMPLEX1:44; :: thesis: verum
end;
suppose (divset ((T . n),i)) /\ (divset ((T . m),j)) <> {} ; :: thesis: |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1))
then consider t being object such that
A97: t in (divset ((T . n),i)) /\ (divset ((T . m),j)) by XBOOLE_0:def 1;
reconsider t = t as Real by A97;
A98: divset ((T . m),j) c= A by A91, INTEGRA1:8;
A99: ( t in divset ((T . n),i) & t in divset ((T . m),j) ) by A97, XBOOLE_0:def 4;
then ( |.((p1 . i) - t).| < sk & |.(t - (p2 . j)).| < sk ) by A20, A91, A93, INTEGR20:12;
then A100: ( |.((u . (p1 . i)) - (u . t)).| < ((p / 2) / ((total_vd rho) + 1)) / 2 & |.((u . t) - (u . (p2 . j))).| < ((p / 2) / ((total_vd rho) + 1)) / 2 ) by A1, A17, A93, A98, A99;
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 = ((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))) + ((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))) by A88, A89, A90, A94;
then A101: |.(Snmij - Smnij).| <= |.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| by COMPLEX1:56;
A102: ( |.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| = |.(vol (DMN,rho)).| * |.((u . (p1 . i)) - (u . t)).| & |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| = |.(vol (DMN,rho)).| * |.((u . t) - (u . (p2 . j))).| ) by COMPLEX1:65;
0 <= |.(vol (DMN,rho)).| by COMPLEX1:46;
then ( |.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| <= |.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2) & |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| <= |.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2) ) by A100, A102, XREAL_1:64;
then |.((vol (DMN,rho)) * ((u . (p1 . i)) - (u . t))).| + |.((vol (DMN,rho)) * ((u . t) - (u . (p2 . j)))).| <= (|.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2)) + (|.(vol (DMN,rho)).| * (((p / 2) / ((total_vd rho) + 1)) / 2)) by XREAL_1:7;
hence |.(Snmij - Smnij).| <= |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| * ((p / 2) / ((total_vd rho) + 1)) by A101, XXREAL_0:2; :: thesis: verum
end;
end;
end;
consider vtntm being FinSequence of REAL such that
A103: ( len vtntm = len (T . m) & Sum vtntm <= total_vd rho & ( for j being Nat st j in dom (T . m) holds
ex p being FinSequence of REAL st
( vtntm . j = Sum p & len p = len (T . n) & ( for i being Nat st i in dom (T . n) holds
p . i = |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) ) ) by A1, Th19;
reconsider PVD = ((p / 2) / ((total_vd rho) + 1)) * vtntm as FinSequence of REAL ;
dom PVD = dom vtntm by VALUED_1:def 5;
then dom PVD = Seg (len (T . m)) by A103, FINSEQ_1:def 3;
then A104: len PVD = len (T . m) by FINSEQ_1:def 3;
A105: for j being Nat st j in Seg (len (T . m)) holds
ex pvtntm being FinSequence of REAL st
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
proof
let j be Nat; :: thesis: ( j in Seg (len (T . m)) implies ex pvtntm being FinSequence of REAL st
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) )
assume j in Seg (len (T . m)) ; :: thesis: ex pvtntm being FinSequence of REAL st
( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
then j in dom (T . m) by FINSEQ_1:def 3;
then consider v being FinSequence of REAL such that
A107: ( vtntm . j = Sum v & len v = len (T . n) & ( for i being Nat st i in dom (T . n) holds
v . i = |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) by A103;
reconsider pvtntm = ((p / 2) / ((total_vd rho) + 1)) * v as FinSequence of REAL ;
take pvtntm ; :: thesis: ( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
thus PVD . j = ((p / 2) / ((total_vd rho) + 1)) * (vtntm . j) by VALUED_1:6
.= Sum pvtntm by A107, RVSUM_1:87 ; :: thesis: ( len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) )
dom pvtntm = dom v by VALUED_1:def 5;
then dom pvtntm = Seg (len (T . n)) by A107, FINSEQ_1:def 3;
hence len pvtntm = len (T . n) by FINSEQ_1:def 3; :: thesis: for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
let i be Nat; :: thesis: ( i in Seg (len (T . n)) implies pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| )
assume i in Seg (len (T . n)) ; :: thesis: pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).|
then a108: i in dom (T . n) by FINSEQ_1:def 3;
thus pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * (v . i) by VALUED_1:6
.= ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| by A107, a108 ; :: thesis: verum
end;
A109: Sum PVD = ((p / 2) / ((total_vd rho) + 1)) * (Sum vtntm) by RVSUM_1:87;
A110: ((p / 2) / ((total_vd rho) + 1)) * (Sum vtntm) <= ((p / 2) / ((total_vd rho) + 1)) * (total_vd rho) by A13, B13, A103, XREAL_1:64;
A111: len XZq = len (T . m) by A56, A68, A84, FINSEQ_1:def 3;
for j being Nat st j in dom XZq holds
|.(XZq . j).| <= PVD . j
proof
let j be Nat; :: thesis: ( j in dom XZq implies |.(XZq . j).| <= PVD . j )
assume A112: j in dom XZq ; :: thesis: |.(XZq . j).| <= PVD . j
then A113: XZq . j = (Xq . j) - (Zq . j) by VALUED_1:13;
consider Xsq being FinSequence of REAL such that
A114: ( 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 A56, A68, A84, A112;
consider Zsq being FinSequence of REAL such that
A115: ( 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 A56, A68, A84, A112;
set XZsq = Xsq - Zsq;
A116: dom (Xsq - Zsq) = (dom Xsq) /\ (dom Zsq) by VALUED_1:12;
reconsider XZsq = Xsq - Zsq as FinSequence of REAL ;
A117: len XZsq = len (T . n) by A114, A115, A116, FINSEQ_1:def 3;
consider pvtntm being FinSequence of REAL such that
A118: ( PVD . j = Sum pvtntm & len pvtntm = len (T . n) & ( for i being Nat st i in Seg (len (T . n)) holds
pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| ) ) by A105, A56, A68, A84, A112;
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 A119: i in dom XZsq ; :: thesis: |.(XZsq . i).| <= pvtntm . i
then A120: XZsq . i = (Xsq . i) - (Zsq . i) by VALUED_1:13;
A121: pvtntm . i = ((p / 2) / ((total_vd rho) + 1)) * |.(vol (((divset ((T . n),i)) /\ (divset ((T . m),j))),rho)).| by A118, A114, A115, A116, A119;
( Xsq . i = Snm . (i,j) & Zsq . i = Smn . (i,j) ) by A114, A115, A116, A119;
hence |.(XZsq . i).| <= pvtntm . i by A56, A68, A84, A87, A112, A114, A115, A116, A119, A120, A121; :: thesis: verum
end;
then A122: |.(Sum XZsq).| <= PVD . j by A117, A118, Th3;
len Xsq = len Zsq by A114, A115, FINSEQ_3:29;
then ( Xsq is Element of (len Xsq) -tuples_on REAL & Zsq is Element of (len Xsq) -tuples_on REAL ) by FINSEQ_2:92;
hence |.(XZq . j).| <= PVD . j by A113, A114, A115, A122, RVSUM_1:90; :: thesis: verum
end;
then |.(Sum XZq).| <= Sum PVD by A104, A111, Th3;
then A124: |.(Sum XZq).| <= (total_vd rho) * ((p / 2) / ((total_vd rho) + 1)) by A109, A110, XXREAL_0:2;
Sum XZq = ((middle_sum S) . n) - ((middle_sum S) . m) by A21, A83, A86, RVSUM_1:90;
hence |.(((middle_sum S) . n) - ((middle_sum S) . m)).| < p by A16, A124, XXREAL_0:2; :: thesis: verum
end;
hence middle_sum S is convergent by SEQ_4:41; :: thesis: verum
end;