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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] )
set W = WellSpace (a,X);
reconsider Xa = [X,a] as Point of (WellSpace (a,X)) by Th37;
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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] )
per cases ( for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex r being Real st
( r > 0 & ( for n being Nat ex m being Nat st
( m >= n & dist ((S . m),Xa) >= r ) ) ) ) ;
suppose for r being Real st r > 0 holds
ex n being Nat st
for m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat ex m being Nat 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat 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 Nat ex m being Nat st
( m >= n & dist ((S . m),Xa) >= r ) ;
consider p being Nat such that
A4: for n, m being Nat st n >= p & m >= p holds
dist ((S . n),(S . m)) < r by A1, A2;
consider p9 being Nat such that
A5: p9 >= p and
A6: dist ((S . p9),Xa) >= r by A3;
consider Y being set , y being Point of M such that
A7: S . p9 = [Y,y] and
( ( Y in X & y <> a ) or ( Y = X & y = a ) ) by Th37;
ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p]
proof
take p9 ; :: thesis: ex Y being set st
for m being Nat st m >= p9 holds
ex p being Point of M st S . m = [Y,p]
take Y ; :: thesis: for m being Nat st m >= p9 holds
ex p being Point of M st S . m = [Y,p]
let m be Nat; :: thesis: ( m >= p9 implies ex p being Point of M st S . m = [Y,p] )
assume A8: m >= p9 ; :: thesis: ex p being Point of M st S . m = [Y,p]
consider Z being set , z being Point of M such that
A9: S . m = [Z,z] and
( ( Z in X & z <> a ) or ( Z = X & z = a ) ) by Th37;
Y = Z
proof
A10: dist (a,z) >= 0 by METRIC_1:5;
A11: dist (a,a) = 0 by METRIC_1:1;
( X = Y or X <> Y ) ;
then ( dist ((S . p9),Xa) = dist (y,a) or dist ((S . p9),Xa) = (dist (y,a)) + 0 ) by A7, A11, Def10;
then A12: (dist (y,a)) + (dist (a,z)) >= r + 0 by A6, A10, XREAL_1:7;
assume Y <> Z ; :: thesis: contradiction
then A13: dist ((S . p9),(S . m)) >= r by A7, A9, A12, Def10;
m >= p by A5, A8, XXREAL_0:2;
hence contradiction by A4, A5, A13; :: thesis: verum
end;
hence ex p being Point of M st S . m = [Y,p] by A9; :: 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 Nat st
for m being Nat st m >= n holds
dist ((S . m),Xa) < r or ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S . m = [Y,p] ) ; :: thesis: verum
end;
end;