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 (delta T) . n = (2 * (vol A)) * ((2 ") |^ (n + 1))

proof

let n be Nat; :: thesis: (delta T) . 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 A1, Def1;
then vol (divset ((EqDiv (A,(2 |^ n))),k)) = (vol A) / (2 |^ n) by A6, Th15;
then (upper_volume ((chi (A,A)),(EqDiv (A,(2 |^ n))))) . k = (vol A) / (2 |^ n) by A6, INTEGRA1:20
.= ((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 A4, XXREAL_2:11; :: thesis: verum

end;

deffunc H₁( Nat) -> object = (2 ") to_power ($1 + 1);
consider seq being Real_Sequence such that
A8: for n being Nat holds seq . n = H₁(n) from SEQ_1:sch 1();
A9: ( seq is convergent & lim seq = 0 ) by A8, SERIES_1:1;
for n being Nat holds (delta T) . n = (2 * (vol A)) * (seq . n)

proof

let n be Nat; :: thesis: (delta T) . 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 A8, SERIES_1:1, SEQ_2:7;
A12: lim (delta T) = (2 * (vol A)) * 0 by A9, A10, SEQ_2:8
.= 0 ;

now :: thesis: not 0 in rng (delta T)

assume 0 in rng (delta T) ; :: thesis: contradiction
then consider m being Element of NAT such that
A13: ( m in dom (delta T) & 0 = (delta T) . m ) by PARTFUN1:3;
A14: (2 * (vol A)) * ((2 ") |^ (m + 1)) = 0 by A3, A13;
( 2 * (vol A) <> 0 & (2 ") |^ (m + 1) <> 0 ) by A1, NEWTON:83;
hence contradiction by A14, XCMPLX_1:6; :: thesis: verum

end;

hence ( delta T is 0 -convergent & delta T is non-zero ) by A11, A12, FDIFF_1:def 1, ORDINAL1:def 15; :: thesis: verum