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 ) )
assume A1: vol A = 0 ; :: thesis: ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 )
set T = the DivSequence of A;
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: len D = 1

proof

assume A4: len D <> 1 ; :: thesis: contradiction
not len D is trivial by A4, 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 & 2 in dom D ) by A5, FINSEQ_3:27;
then A7: D . 1 < D . 2 by SEQM_3:def 1;
( D . 1 in A & D . 2 in A ) by A6, INTEGRA1:8;
then A8: ( lower_bound A <= D . 1 & D . 1 <= upper_bound A & lower_bound A <= D . 2 & D . 2 <= upper_bound A ) by INTEGRA2:1;
(upper_bound A) - (lower_bound A) = 0 by A1, INTEGRA1:def 6;
hence contradiction by A7, A8, XXREAL_0:1; :: thesis: verum

end;

A9: (delta the DivSequence of A) . i = delta D by INTEGRA2:def 3
.= max (rng (upper_volume (chi A,A),D)) by INTEGRA1:def 19 ;
rng (upper_volume (chi A,A),D) = {0 }

proof

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 A10: x1 in rng (upper_volume (chi A,A),D) ; :: thesis: x1 in {0 }
then consider k being Element of NAT such that
A11: ( k in dom (upper_volume (chi A,A),D) & (upper_volume (chi A,A),D) . k = x1 ) by PARTFUN1:26;
reconsider x1 = x1 as Real by A10;
k in Seg (len (upper_volume (chi A,A),D)) by A11, FINSEQ_1:def 3;
then A12: k in Seg (len D) by INTEGRA1:def 7;
then k in dom D by FINSEQ_1:def 3;
then A13: x1 = vol (divset D,k) by A11, INTEGRA1:22;
then A14: x1 >= 0 by INTEGRA1:11;
k in dom D by A12, FINSEQ_1:def 3;
then x1 = 0 by A1, A13, A14, INTEGRA1:10, INTEGRA2:40;
hence x1 in {0 } by TARSKI:def 1; :: thesis: verum

end;

then A15: rng (upper_volume (chi A,A),D) c= {0 } by TARSKI:def 3;
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) )
assume A16: x1 in {0 } ; :: thesis: x1 in rng (upper_volume (chi A,A),D)
A17: 1 in Seg (len D) by A3, FINSEQ_1:5;
then B17: 1 in dom D by FINSEQ_1:def 3;
1 in Seg (len (upper_volume (chi A,A),D)) by A17, INTEGRA1:def 7;
then 1 in dom (upper_volume (chi A,A),D) by FINSEQ_1:def 3;
then A18: (upper_volume (chi A,A),D) . 1 in rng (upper_volume (chi A,A),D) by FUNCT_1:def 5;
A19: (upper_volume (chi A,A),D) . 1 = vol (divset D,1) by B17, INTEGRA1:22;
( upper_bound (divset D,1) = upper_bound A & lower_bound (divset D,1) = lower_bound A )

proof

1 in dom D by A17, FINSEQ_1:def 3;
then ( upper_bound (divset D,1) = D . (len D) & lower_bound (divset D,1) = lower_bound A ) by A3, INTEGRA1:def 5;
hence ( upper_bound (divset D,1) = upper_bound A & lower_bound (divset D,1) = lower_bound A ) by INTEGRA1:def 2; :: thesis: verum

end;

then vol (divset D,1) = (upper_bound A) - (lower_bound A) by INTEGRA1:def 6
.= 0 by A1, INTEGRA1:def 6 ;
hence x1 in rng (upper_volume (chi A,A),D) by A16, A18, A19, TARSKI:def 1; :: thesis: verum

end;

then {0 } c= rng (upper_volume (chi A,A),D) by TARSKI:def 3;
hence rng (upper_volume (chi A,A),D) = {0 } by A15, XBOOLE_0:def 10; :: thesis: verum

end;

then (delta the DivSequence of A) . i in {0 } by A9, XXREAL_2:def 8;
hence (delta the DivSequence of A) . i = 0 by TARSKI:def 1; :: thesis: verum

end;

then A20: 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 A20, SEQ_4:40;
hence ex T being DivSequence of A st
( delta T is convergent & lim (delta T) = 0 ) by A20; :: thesis: verum