let M be non empty Reflexive MetrStruct ; for S being pointwise_bounded SetSequence of M st S is non-ascending & lim (diameter S) = 0 holds
for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy
let S be pointwise_bounded SetSequence of M; ( S is non-ascending & lim (diameter S) = 0 implies for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy )
assume that
A1:
S is non-ascending
and
A2:
lim (diameter S) = 0
; for F being sequence of M st ( for i being Nat holds F . i in S . i ) holds
F is Cauchy
set d = diameter S;
A3:
diameter S is non-increasing
by A1, Th2;
A4:
diameter S is bounded_below
by Th1;
let F be sequence of M; ( ( for i being Nat holds F . i in S . i ) implies F is Cauchy )
assume A5:
for i being Nat holds F . i in S . i
; F is Cauchy
let r be Real; TBSP_1:def 4 ( r <= 0 or ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((F . b2),(F . b3)) ) )
assume
r > 0
; ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((F . b2),(F . b3)) )
then consider n being Nat such that
A6:
for m being Nat st n <= m holds
|.(((diameter S) . m) - 0).| < r
by A2, A4, A3, SEQ_2:def 7;
take
n
; for b1, b2 being set holds
( not n <= b1 or not n <= b2 or not r <= dist ((F . b1),(F . b2)) )
let m1, m2 be Nat; ( not n <= m1 or not n <= m2 or not r <= dist ((F . m1),(F . m2)) )
assume that
A7:
n <= m1
and
A8:
n <= m2
; not r <= dist ((F . m1),(F . m2))
A9:
S . m2 c= S . n
by A1, A8, PROB_1:def 4;
A10:
F . m2 in S . m2
by A5;
A11:
F . m1 in S . m1
by A5;
A12:
|.(((diameter S) . n) - 0).| < r
by A6;
A13:
diameter (S . n) = (diameter S) . n
by Def2;
A14:
S . n is bounded
by Def1;
then
0 <= (diameter S) . n
by A13, TBSP_1:21;
then A15:
(diameter S) . n < r
by A12, ABSVALUE:def 1;
S . m1 c= S . n
by A1, A7, PROB_1:def 4;
then
dist ((F . m1),(F . m2)) <= (diameter S) . n
by A9, A11, A10, A14, A13, TBSP_1:def 8;
hence
not r <= dist ((F . m1),(F . m2))
by A15, XXREAL_0:2; verum