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 )
set A = rng S1;
assume S1 is Cauchy ; :: thesis: rng S1 is bounded
then consider p being Nat such that
A1: for n, m being Nat st p <= n & p <= m holds
dist ((S1 . n),(S1 . m)) < 1 ;
defpred S₁[ set ] means ex n being 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 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 ;
A2: C is finite

proof

set K = Seg p;
set J = {0} \/ (Seg p);

now :: thesis: for x being object holds
( ( x in C implies x in S1 .: ({0} \/ (Seg p)) ) & ( x in S1 .: ({0} \/ (Seg p)) implies x in C ) )

let x be object ; :: 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 and
A4: ex n being Nat st
( n <= p & t1 = S1 . n ) ;
consider n being Nat such that
A5: n <= p and
A6: t1 = S1 . n by A4;
n in NAT by ORDINAL1:def 12;
then A7: n in dom S1 by FUNCT_2:def 1;

now :: thesis: x in S1 .: ({0} \/ (Seg p))

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, A6, A7, FUNCT_1:def 6; :: thesis: verum

end;

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

then 1 <= n by NAT_1:11;
then n in { k where k is Nat : ( 1 <= k & k <= p ) } by A5;
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, A6, A7, FUNCT_1:def 6; :: 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 object such that
A8: y in dom S1 and
A9: y in {0} \/ (Seg p) and
A10: x = S1 . y by FUNCT_1:def 6;
reconsider y = y as Nat by A8;

now :: thesis: x in C

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

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

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

end;

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

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

end;

end;

end;

hence x in C ; :: thesis: verum

end;

hence C is finite by TARSKI:2; :: thesis: verum

end;

A13: 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 object ; :: 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 object such that
A14: y in dom S1 and
A15: x = S1 . y by FUNCT_1:def 3;
reconsider y = y as Nat by A14;
S1 . y is Element of T ;
then reconsider x9 = x as Element of T by A15;

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

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

then ex n being Nat st
( n <= p & x9 = S1 . n ) by A15;
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 Nat st
( p <= n & x9 = S1 . n ) by A15;
then x in B ;
hence x in B \/ C by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

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

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

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

end;

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

then consider t1 being Element of T such that
A20: x = t1 and
A21: ex n being Nat st
( n <= p & t1 = S1 . n ) ;
consider n being Nat such that
n <= p and
A22: t1 = S1 . n by A21;
n in NAT by ORDINAL1:def 12;
then n in dom S1 by FUNCT_2:def 1;
hence x in rng S1 by A20, A22, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

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 ex t1 being Element of T st
( z = t1 & ex n being Nat st
( p <= n & t1 = S1 . n ) ) ;
hence dist ((S1 . p),z) <= 1 by A1; :: thesis: verum

end;

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

end;

hence rng S1 is bounded by A2, A13, Th13; :: thesis: verum