let X be set ; :: thesis: for M being non empty Reflexive symmetric triangle MetrStruct
for a being Point of M
for S being sequence of (WellSpace a,X) holds
( not S is Cauchy or for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for a being Point of M
for S being sequence of (WellSpace a,X) holds
( not S is Cauchy or for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )
let a be Point of M; :: thesis: for S being sequence of (WellSpace a,X) holds
( not S is Cauchy or for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )
set W = WellSpace a,X;
let S be sequence of (WellSpace a,X); :: thesis: ( not S is Cauchy or for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )
assume A1: S is Cauchy ; :: thesis: ( for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )
reconsider Xa = [X,a] as Point of (WellSpace a,X) by Th38;

per cases ( for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex r being Real st
( r > 0 & ( for n being natural number ex m being natural number st
( m >= n & dist (S . m),Xa >= r ) ) ) ) ;

suppose for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r ; :: thesis: ( for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )

hence ( for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] ) ; :: thesis: verum

end;

suppose ex r being Real st
( r > 0 & ( for n being natural number ex m being natural number st
( m >= n & dist (S . m),Xa >= r ) ) ) ; :: thesis: ( for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] )

then consider r being Real such that
A2: r > 0 and
A3: for n being natural number ex m being natural number st
( m >= n & dist (S . m),Xa >= r ) ;
consider p being Element of NAT such that
A4: for n, m being Element of NAT st n >= p & m >= p holds
dist (S . n),(S . m) < r by A1, A2, TBSP_1:def 5;
consider p' being natural number such that
A5: ( p' >= p & dist (S . p'),Xa >= r ) by A3;
consider Y being set , y being Point of M such that
A6: ( S . p' = [Y,y] & ( ( Y in X & y <> a ) or ( Y = X & y = a ) ) ) by Th38;
ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p]

proof

take p' ; :: thesis: ex Y being set st
for m being natural number st m >= p' holds
ex p being Point of M st S . m = [Y,p]
take Y ; :: thesis: for m being natural number st m >= p' holds
ex p being Point of M st S . m = [Y,p]
let m be natural number ; :: thesis: ( m >= p' implies ex p being Point of M st S . m = [Y,p] )
assume A7: m >= p' ; :: thesis: ex p being Point of M st S . m = [Y,p]
consider Z being set , z being Point of M such that
A8: ( S . m = [Z,z] & ( ( Z in X & z <> a ) or ( Z = X & z = a ) ) ) by Th38;
Y = Z

proof

assume A9: Y <> Z ; :: thesis: contradiction
( ( X = Y or X <> Y ) & dist a,a = 0 ) by METRIC_1:1;
then ( dist (S . p'),Xa = dist y,a or dist (S . p'),Xa = (dist y,a) + 0 ) by A6, Def10;
then ( dist y,a >= r & dist a,z >= 0 ) by A5, METRIC_1:5;
then ( (dist y,a) + (dist a,z) >= r + 0 & m >= p & m in NAT & p' in NAT ) by A5, A7, ORDINAL1:def 13, XREAL_1:9, XXREAL_0:2;
then ( dist (S . p'),(S . m) >= r & dist (S . p'),(S . m) < r ) by A4, A5, A6, A8, A9, Def10;
hence contradiction ; :: thesis: verum

end;

hence ex p being Point of M st S . m = [Y,p] by A8; :: thesis: verum

end;

hence ( for Xa being Point of (WellSpace a,X) st Xa = [X,a] holds
for r being Real st r > 0 holds
ex n being natural number st
for m being natural number st m >= n holds
dist (S . m),Xa < r or ex n being natural number ex Y being set st
for m being natural number st m >= n holds
ex p being Point of M st S . m = [Y,p] ) ; :: thesis: verum

end;

end;