let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for S1 being sequence of T st S1 is Cauchy holds
rng S1 is bounded
let S1 be sequence of T; :: thesis: ( S1 is Cauchy implies rng S1 is bounded )
assume A1: S1 is Cauchy ; :: thesis: rng S1 is bounded
set A = rng S1;
consider p being Element of NAT such that
A2: for n, m being Element of NAT st p <= n & p <= m holds
dist (S1 . n),(S1 . m) < 1 by A1, Def5;
defpred S₁[ set ] means ex n being Element of NAT st
( p <= n & $1 = S1 . n );
reconsider B = { t1 where t1 is Point of T : S₁[t1] } as Subset of T from DOMAIN_1:sch 7();
defpred S₂[ set ] means ex n being Element of NAT st
( n <= p & $1 = S1 . n );
reconsider C = { t1 where t1 is Point of T : S₂[t1] } as Subset of T from DOMAIN_1:sch 7();
reconsider B = B, C = C as Subset of T ;
C is finite

proof

set K = Seg p;
set J = {0 } \/ (Seg p);
C = S1 .: ({0 } \/ (Seg p))

proof

now

let x be set ; :: thesis: ( ( x in C implies x in S1 .: ({0 } \/ (Seg p)) ) & ( x in S1 .: ({0 } \/ (Seg p)) implies x in C ) )
thus ( x in C implies x in S1 .: ({0 } \/ (Seg p)) ) :: thesis: ( x in S1 .: ({0 } \/ (Seg p)) implies x in C )

proof

assume x in C ; :: thesis: x in S1 .: ({0 } \/ (Seg p))
then consider t1 being Element of T such that
A3: ( x = t1 & ex n being Element of NAT st
( n <= p & t1 = S1 . n ) ) ;
consider n being Element of NAT such that
A4: ( n <= p & t1 = S1 . n ) by A3;
n in NAT ;
then A5: n in dom S1 by FUNCT_2:def 1;

now

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: x in S1 .: ({0 } \/ (Seg p))

then n in {0 } by TARSKI:def 1;
then n in {0 } \/ (Seg p) by XBOOLE_0:def 3;
hence x in S1 .: ({0 } \/ (Seg p)) by A3, A4, A5, FUNCT_1:def 12; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: x in S1 .: ({0 } \/ (Seg p))

then consider m being Nat such that
A6: n = m + 1 ;
1 <= n by A6, NAT_1:11;
then n in { k where k is Element of NAT : ( 1 <= k & k <= p ) } by A4;
then n in Seg p by FINSEQ_1:def 1;
then n in {0 } \/ (Seg p) by XBOOLE_0:def 3;
hence x in S1 .: ({0 } \/ (Seg p)) by A3, A4, A5, FUNCT_1:def 12; :: thesis: verum

end;

end;

end;

hence x in S1 .: ({0 } \/ (Seg p)) ; :: thesis: verum

end;

assume x in S1 .: ({0 } \/ (Seg p)) ; :: thesis: x in C
then consider y being set such that
A7: ( y in dom S1 & y in {0 } \/ (Seg p) & x = S1 . y ) by FUNCT_1:def 12;
reconsider y = y as Element of NAT by A7;

now

per cases ( y in {0 } or y in Seg p ) by A7, XBOOLE_0:def 3;

suppose y in {0 } ; :: thesis: x in C

then A8: y = 0 by TARSKI:def 1;
S1 . y is Element of T ;
then reconsider x' = x as Element of T by A7;
ex n being Element of NAT st
( n <= p & x' = S1 . n ) by A7, A8;
hence x in C ; :: thesis: verum

end;

suppose y in Seg p ; :: thesis: x in C

then y in { k where k is Element of NAT : ( 1 <= k & k <= p ) } by FINSEQ_1:def 1;
then A9: ex k being Element of NAT st
( y = k & 1 <= k & k <= p ) ;
S1 . y is Element of T ;
then reconsider x' = x as Element of T by A7;
ex n being Element of NAT st
( n <= p & x' = S1 . n ) by A7, A9;
hence x in C ; :: thesis: verum

end;

end;

end;

hence x in C ; :: thesis: verum

end;

hence C = S1 .: ({0 } \/ (Seg p)) by TARSKI:2; :: thesis: verum

end;

hence C is finite ; :: thesis: verum

end;

then A10: C is bounded ;
A11: B is bounded

proof

set x = S1 . p;
ex r being Real ex t1 being Element of T st
( 0 < r & t1 in B & ( for z being Point of T st z in B holds
dist t1,z <= r ) )

proof

take 1 ; :: thesis: ex t1 being Element of T st
( 0 < 1 & t1 in B & ( for z being Point of T st z in B holds
dist t1,z <= 1 ) )
take S1 . p ; :: thesis: ( 0 < 1 & S1 . p in B & ( for z being Point of T st z in B holds
dist (S1 . p),z <= 1 ) )
thus 0 < 1 ; :: thesis: ( S1 . p in B & ( for z being Point of T st z in B holds
dist (S1 . p),z <= 1 ) )
thus S1 . p in B ; :: thesis: for z being Point of T st z in B holds
dist (S1 . p),z <= 1
let z be Point of T; :: thesis: ( z in B implies dist (S1 . p),z <= 1 )
assume z in B ; :: thesis: dist (S1 . p),z <= 1
then consider t1 being Element of T such that
A12: ( z = t1 & ex n being Element of NAT st
( p <= n & t1 = S1 . n ) ) ;
thus dist (S1 . p),z <= 1 by A2, A12; :: thesis: verum

end;

hence B is bounded by Th15; :: thesis: verum

end;

rng S1 = B \/ C

proof

thus rng S1 c= B \/ C :: according to XBOOLE_0:def 10 :: thesis: B \/ C c= rng S1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng S1 or x in B \/ C )
assume x in rng S1 ; :: thesis: x in B \/ C
then consider y being set such that
A13: ( y in dom S1 & x = S1 . y ) by FUNCT_1:def 5;
reconsider y = y as Element of NAT by A13;
S1 . y is Element of T ;
then reconsider x' = x as Element of T by A13;

per cases ( y <= p or p <= y ) ;

suppose y <= p ; :: thesis: x in B \/ C

then ex n being Element of NAT st
( n <= p & x' = S1 . n ) by A13;
then x in C ;
hence x in B \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

suppose p <= y ; :: thesis: x in B \/ C

then ex n being Element of NAT st
( p <= n & x' = S1 . n ) by A13;
then x in B ;
hence x in B \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B \/ C or x in rng S1 )
assume A14: x in B \/ C ; :: thesis: x in rng S1

per cases ( x in B or x in C ) by A14, XBOOLE_0:def 3;

suppose x in B ; :: thesis: x in rng S1

then consider t1 being Element of T such that
A15: ( x = t1 & ex n being Element of NAT st
( p <= n & t1 = S1 . n ) ) ;
consider n being Element of NAT such that
A16: ( p <= n & t1 = S1 . n ) by A15;
n in NAT ;
then n in dom S1 by FUNCT_2:def 1;
hence x in rng S1 by A15, A16, FUNCT_1:def 5; :: thesis: verum

end;

suppose x in C ; :: thesis: x in rng S1

then consider t1 being Element of T such that
A17: ( x = t1 & ex n being Element of NAT st
( n <= p & t1 = S1 . n ) ) ;
consider n being Element of NAT such that
A18: ( n <= p & t1 = S1 . n ) by A17;
n in NAT ;
then n in dom S1 by FUNCT_2:def 1;
hence x in rng S1 by A17, A18, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence rng S1 is bounded by A10, A11, Th20; :: thesis: verum