let A be non empty closed_interval Subset of REAL; :: thesis: for T being sequence of (divs A) st vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) holds
( delta T is 0 -convergent & delta T is non-zero )

let T be sequence of (divs A); :: thesis: ( vol A > 0 & ( for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ) implies ( delta T is 0 -convergent & delta T is non-zero ) )
assume that
A1: vol A > 0 and
A2: for n being Nat holds T . n = EqDiv (A,(2 |^ n)) ; :: thesis: ( delta T is 0 -convergent & delta T is non-zero )
A3: for n being Nat holds () . n = (2 * (vol A)) * ((2 ") |^ (n + 1))
proof
let n be Nat; :: thesis: () . n = (2 * (vol A)) * ((2 ") |^ (n + 1))
n is Element of NAT by ORDINAL1:def 12;
then (delta T) . n = delta (T . n) by INTEGRA3:def 2;
then (delta T) . n = delta (EqDiv (A,(2 |^ n))) by A2;
then A4: (delta T) . n = max (rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n)))))) by INTEGRA3:def 1;
A5: for k being Nat st k in dom (EqDiv (A,(2 |^ n))) holds
(upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))
proof
let k be Nat; :: thesis: ( k in dom (EqDiv (A,(2 |^ n))) implies (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) )
assume A6: k in dom (EqDiv (A,(2 |^ n))) ; :: thesis: (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1))
2 |^ n > 0 by NEWTON:83;
then EqDiv (A,(2 |^ n)) divide_into_equal 2 |^ n by ;
then vol (divset ((EqDiv (A,(2 |^ n))),k)) = (vol A) / (2 |^ n) by ;
then (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (vol A) / (2 |^ n) by
.= ((vol A) / ((2 |^ n) * 2)) * 2 by XCMPLX_1:92
.= ((vol A) / (2 |^ (n + 1))) * 2 by NEWTON:6
.= ((vol A) * ((2 |^ (n + 1)) ")) * 2 by XCMPLX_0:def 9
.= (2 * (vol A)) * ((2 |^ (n + 1)) ") ;
hence (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (2 * (vol A)) * ((2 ") |^ (n + 1)) by Th16; :: thesis: verum
end;
now :: thesis: for q being object st q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) holds
q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
let q be object ; :: thesis: ( q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) implies q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} )
assume q in rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) ; :: thesis: q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))}
then consider p being Element of NAT such that
A7: ( p in dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) & q = (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . p ) by PARTFUN1:3;
len (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = len (EqDiv (A,(2 |^ n))) by INTEGRA1:def 6;
then dom (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = dom (EqDiv (A,(2 |^ n))) by FINSEQ_3:29;
then q = (2 * (vol A)) * ((2 ") |^ (n + 1)) by A5, A7;
hence q in {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by TARSKI:def 1; :: thesis: verum
end;
then rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) c= {((2 * (vol A)) * ((2 ") |^ (n + 1)))} ;
then rng (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) = {((2 * (vol A)) * ((2 ") |^ (n + 1)))} by ZFMISC_1:33;
hence (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1)) by ; :: thesis: verum
end;
deffunc H1( Nat) -> object = (2 ") to_power (\$1 + 1);
consider seq being Real_Sequence such that
A8: for n being Nat holds seq . n = H1(n) from SEQ_1:sch 1();
A9: ( seq is convergent & lim seq = 0 ) by ;
for n being Nat holds () . n = (2 * (vol A)) * (seq . n)
proof
let n be Nat; :: thesis: () . n = (2 * (vol A)) * (seq . n)
seq . n = (2 ") to_power (n + 1) by A8
.= (2 ") |^ (n + 1) by POWER:41 ;
hence (delta T) . n = (2 * (vol A)) * (seq . n) by A3; :: thesis: verum
end;
then A10: delta T = (2 * (vol A)) (#) seq by SEQ_1:9;
then A11: delta T is convergent by ;
A12: lim () = (2 * (vol A)) * 0 by
.= 0 ;
now :: thesis: not 0 in rng ()
assume 0 in rng () ; :: thesis: contradiction
then consider m being Element of NAT such that
A13: ( m in dom () & 0 = () . m ) by PARTFUN1:3;
A14: (2 * (vol A)) * ((2 ") |^ (m + 1)) = 0 by ;
( 2 * (vol A) <> 0 & (2 ") |^ (m + 1) <> 0 ) by ;
hence contradiction by A14, XCMPLX_1:6; :: thesis: verum
end;
hence ( delta T is 0 -convergent & delta T is non-zero ) by ; :: thesis: verum