let A be non empty closed_interval Subset of REAL; ( 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
; 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;
(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
for
x1 being
object st
x1 in {0} holds
x1 in rng (upper_volume ((chi (A,A)),D))
proof
let x1 be
object ;
( 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}
;
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;
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 ;
( x1 in rng (upper_volume ((chi (A,A)),D)) implies x1 in {0} )
assume A20:
x1 in rng (upper_volume ((chi (A,A)),D))
;
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;
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;
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; verum