let X be set ; 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 ; 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; 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)); ( 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
; ( 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
ex
r being
Real st
(
r > 0 & ( for
n being
Nat ex
m being
Nat st
(
m >= n &
dist (
(S . m),
Xa)
>= r ) ) )
;
( 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
;
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
;
for m being Nat st m >= p9 holds
ex p being Point of M st S . m = [Y,p]
let m be
Nat;
( m >= p9 implies ex p being Point of M st S . m = [Y,p] )
assume A8:
m >= p9
;
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
;
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;
verum
end;
hence
ex
p being
Point of
M st
S . m = [Y,p]
by A9;
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] )
;
verum end; end;