let A be 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 = 0

proof

let i be Nat; :: thesis: (delta the DivSequence of A) . i = 0
reconsider ii = i as Element of NAT by ORDINAL1:def 13;
reconsider D = the DivSequence of A . ii as Division of A ;
A3: (delta the DivSequence of A) . i = delta D by INTEGRA2:def 3
.= max (rng (upper_volume (chi A,A),D)) by INTEGRA1:def 19 ;
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:31;
then 1 <= len D by XXREAL_0:2;
then A6: 1 in dom D by FINSEQ_3:27;
then A7: D . 1 in A by INTEGRA1:8;
then A8: lower_bound A <= D . 1 by INTEGRA2:1;
A9: 2 in dom D by A5, FINSEQ_3:27;
then D . 2 in A by INTEGRA1:8;
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 6;
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 set st x1 in {0 } holds
x1 in rng (upper_volume (chi A,A),D)

proof

let x1 be set ; :: thesis: ( x1 in {0 } implies x1 in rng (upper_volume (chi A,A),D) )
A13: 1 in Seg (len D) by A4, FINSEQ_1:5;
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:22;
1 in Seg (len (upper_volume (chi A,A),D)) by A13, INTEGRA1:def 7;
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 5;
A16: 1 in dom D by A13, FINSEQ_1:def 3;
then upper_bound (divset D,1) = D . (len D) by A4, INTEGRA1:def 5;
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 5;
then A18: vol (divset D,1) = (upper_bound A) - (lower_bound A) by A17, INTEGRA1:def 6
.= 0 by A1, INTEGRA1:def 6 ;
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 set st x1 in rng (upper_volume (chi A,A),D) holds
x1 in {0 }

proof

let x1 be set ; :: 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:26;
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 7;
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:22;
then x1 >= 0 by INTEGRA1:11;
then x1 = 0 by A1, A25, A24, INTEGRA1:10, INTEGRA2:40;
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 = 0 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:40;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A26; :: thesis: verum