let A be non empty closed_interval Subset of REAL; :: thesis: ( vol A = 0 implies ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) )
set T = the DivSequence of A;
assume A1: vol A = 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
A2: for i being Nat holds (delta the DivSequence of A) . i = In (0,REAL)

proof

let i be Nat; :: thesis: (delta the DivSequence of A) . i = In (0,REAL)
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
reconsider D = the DivSequence of A . ii as Division of A ;
A3: (delta the DivSequence of A) . i = delta D by INTEGRA3:def 2
.= max (rng (upper_volume ((chi (A,A)),D))) by INTEGRA3:def 1 ;
A4: len D = 1

proof

assume len D <> 1 ; :: thesis: contradiction
then not len D is trivial by NAT_2:def 1;
then A5: len D >= 2 by NAT_2:29;
then 1 <= len D by XXREAL_0:2;
then A6: 1 in dom D by FINSEQ_3:25;
then A7: D . 1 in A by INTEGRA1:6;
then A8: lower_bound A <= D . 1 by INTEGRA2:1;
A9: 2 in dom D by A5, FINSEQ_3:25;
then D . 2 in A by INTEGRA1:6;
then A10: D . 2 <= upper_bound A by INTEGRA2:1;
A11: D . 1 <= upper_bound A by A7, INTEGRA2:1;
A12: (upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def 5;
D . 1 < D . 2 by A6, A9, SEQM_3:def 1;
hence contradiction by A8, A11, A10, A12, XXREAL_0:1; :: thesis: verum

end;

for x1 being object st x1 in {0} holds
x1 in rng (upper_volume ((chi (A,A)),D))

proof

let x1 be object ; :: thesis: ( x1 in {0} implies x1 in rng (upper_volume ((chi (A,A)),D)) )
A13: 1 in Seg (len D) by A4, FINSEQ_1:3;
then 1 in dom D by FINSEQ_1:def 3;
then A14: (upper_volume ((chi (A,A)),D)) . 1 = vol (divset (D,1)) by INTEGRA1:20;
1 in Seg (len (upper_volume ((chi (A,A)),D))) by A13, INTEGRA1:def 6;
then 1 in dom (upper_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
then A15: (upper_volume ((chi (A,A)),D)) . 1 in rng (upper_volume ((chi (A,A)),D)) by FUNCT_1:def 3;
A16: 1 in dom D by A13, FINSEQ_1:def 3;
then upper_bound (divset (D,1)) = D . (len D) by A4, INTEGRA1:def 4;
then A17: upper_bound (divset (D,1)) = upper_bound A by INTEGRA1:def 2;
lower_bound (divset (D,1)) = lower_bound A by A16, INTEGRA1:def 4;
then A18: vol (divset (D,1)) = (upper_bound A) - (lower_bound A) by A17, INTEGRA1:def 5
.= 0 by A1, INTEGRA1:def 5 ;
assume x1 in {0} ; :: thesis: x1 in rng (upper_volume ((chi (A,A)),D))
hence x1 in rng (upper_volume ((chi (A,A)),D)) by A15, A14, A18, TARSKI:def 1; :: thesis: verum

end;

then A19: {0} c= rng (upper_volume ((chi (A,A)),D)) by TARSKI:def 3;
for x1 being object st x1 in rng (upper_volume ((chi (A,A)),D)) holds
x1 in {0}

proof

let x1 be object ; :: thesis: ( x1 in rng (upper_volume ((chi (A,A)),D)) implies x1 in {0} )
assume A20: x1 in rng (upper_volume ((chi (A,A)),D)) ; :: thesis: x1 in {0}
then consider k being Element of NAT such that
A21: k in dom (upper_volume ((chi (A,A)),D)) and
A22: (upper_volume ((chi (A,A)),D)) . k = x1 by PARTFUN1:3;
reconsider x1 = x1 as Real by A20;
k in Seg (len (upper_volume ((chi (A,A)),D))) by A21, FINSEQ_1:def 3;
then A23: k in Seg (len D) by INTEGRA1:def 6;
then A24: k in dom D by FINSEQ_1:def 3;
k in dom D by A23, FINSEQ_1:def 3;
then A25: x1 = vol (divset (D,k)) by A22, INTEGRA1:20;
then x1 >= 0 by INTEGRA1:9;
then x1 = 0 by A1, A25, A24, INTEGRA1:8, INTEGRA2:38;
hence x1 in {0} by TARSKI:def 1; :: thesis: verum

end;

then rng (upper_volume ((chi (A,A)),D)) c= {0} by TARSKI:def 3;
then rng (upper_volume ((chi (A,A)),D)) = {0} by A19, XBOOLE_0:def 10;
then (delta the DivSequence of A) . i in {0} by A3, XXREAL_2:def 8;
hence (delta the DivSequence of A) . i = In (0,REAL) by TARSKI:def 1; :: thesis: verum

end;

then A26: delta the DivSequence of A is constant by VALUED_0:def 18;
(delta the DivSequence of A) . 1 = 0 by A2;
then lim (delta the DivSequence of A) = 0 by A26, SEQ_4:25;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A26; :: thesis: verum