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 S1[ set ] means ex n being Nat st
( p <= n & \$1 = S1 . n );
reconsider B = { t1 where t1 is Point of T : S1[t1] } as Subset of T from defpred S2[ set ] means ex n being Nat st
( n <= p & \$1 = S1 . n );
reconsider C = { t1 where t1 is Point of T : S2[t1] } as Subset of T from reconsider B = B, C = C as Subset of T ;
A2: C is finite
proof
set K = Seg p;
set J = \/ (Seg p);
now :: thesis: for x being object holds
( ( x in C implies x in S1 .: ( \/ (Seg p)) ) & ( x in S1 .: ( \/ (Seg p)) implies x in C ) )
let x be object ; :: thesis: ( ( x in C implies x in S1 .: ( \/ (Seg p)) ) & ( x in S1 .: ( \/ (Seg p)) implies x in C ) )
thus ( x in C implies x in S1 .: ( \/ (Seg p)) ) :: thesis: ( x in S1 .: ( \/ (Seg p)) implies x in C )
proof
assume x in C ; :: thesis: x in S1 .: ( \/ (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 .: ( \/ (Seg p))
per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;
suppose ex m being Nat st n = m + 1 ; :: thesis: x in S1 .: ( \/ (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 \/ (Seg p) by XBOOLE_0:def 3;
hence x in S1 .: ( \/ (Seg p)) by ; :: thesis: verum
end;
end;
end;
hence x in S1 .: ( \/ (Seg p)) ; :: thesis: verum
end;
assume x in S1 .: ( \/ (Seg p)) ; :: thesis: x in C
then consider y being object such that
A8: y in dom S1 and
A9: y in \/ (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 or y in Seg p ) by ;
suppose A11: y in ; :: thesis: x in C
S1 . y is Element of T ;
then reconsider x9 = x as Element of T by A10;
y = 0 by ;
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 ;
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 ;
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 ; :: 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 ; :: 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 ; :: thesis: verum