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_{1}[ set ] means ex n being Nat st

( p <= n & $1 = S1 . n );

reconsider B = { t1 where t1 is Point of T : S_{1}[t1] } as Subset of T from DOMAIN_1:sch 7();

defpred S_{2}[ set ] means ex n being Nat st

( n <= p & $1 = S1 . n );

reconsider C = { t1 where t1 is Point of T : S_{2}[t1] } as Subset of T from DOMAIN_1:sch 7();

reconsider B = B, C = C as Subset of T ;

A2: C is finite

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

( p <= n & $1 = S1 . n );

reconsider B = { t1 where t1 is Point of T : S

defpred S

( n <= p & $1 = S1 . n );

reconsider C = { t1 where t1 is Point of T : S

reconsider B = B, C = C as Subset of T ;

A2: C is finite

proof

A13:
rng S1 = B \/ C
set K = Seg p;

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

end;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 ) )

hence
C is finite
by TARSKI:2; :: thesis: verum( ( 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 )

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;

end;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 S1 .: ({0} \/ (Seg p))
; :: thesis: x in C
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;

end;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))end;

hence
x in S1 .: ({0} \/ (Seg p))
; :: thesis: verumper cases
( n = 0 or ex m being Nat st n = m + 1 )
by NAT_1:6;

end;

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;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

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;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

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 Cend;

hence
x in C
; :: thesis: verumper cases
( y in {0} or y in Seg p )
by A9, XBOOLE_0:def 3;

end;

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;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

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;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

proof

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

assume A16: x in B \/ C ; :: thesis: x in rng S1

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B \/ C or x in rng S1 )
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;

end;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 )
;

end;

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;( n <= p & x9 = S1 . n ) by A15;

then x in C ;

hence x in B \/ C by XBOOLE_0:def 3; :: thesis: verum

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;( p <= n & x9 = S1 . n ) by A15;

then x in B ;

hence x in B \/ C by XBOOLE_0:def 3; :: thesis: verum

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;

end;

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;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

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;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

proof

hence
rng S1 is bounded
by A2, A13, Th13; :: thesis: verum
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 ) )

end;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

hence
B is bounded
by Th10; :: thesis: verum
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;( 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