let X be set ; :: thesis:
let M be non empty Reflexive symmetric triangle MetrStruct ; :: thesis:
let a be Point of M; :: thesis:
set W = WellSpace (a,X);
reconsider Xa = [X,a] as Point of (WellSpace (a,X)) by Th37;
assume A1: M is complete ; :: thesis:
let S9 be sequence of (WellSpace (a,X)); :: according to TBSP_1:def 5 :: thesis:
assume A2: S9 is Cauchy ; :: thesis:
defpred S₁[ object , object ] means ex x being set st S9 . $1 = [x,$2];
A3: for x being object st x in NAT holds
ex y being object st
( y in the carrier of M & S₁[x,y] )

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Nat ;
consider s1 being set , s2 being Point of M such that
A4: S9 . i = [s1,s2] and
( ( s1 in X & s2 <> a ) or ( s1 = X & s2 = a ) ) by Th37;
take s2 ; :: thesis:
thus ( s2 in the carrier of M & S₁[x,s2] ) by A4; :: thesis:

end;

consider S being sequence of M such that
A5: for x being object st x in NAT holds
S₁[x,S . x] from FUNCT_2:sch 1(A3);
S is Cauchy

let r be Real; :: according to TBSP_1:def 4 :: thesis:
assume r > 0 ; :: thesis:
then consider p being Nat such that
A6: for n, m being Nat st p <= n & p <= m holds
dist ((S9 . n),(S9 . m)) < r by A2;
take p ; :: thesis:
let n, m be Nat; :: thesis:
assume that
A7: p <= n and
A8: p <= m ; :: thesis:
A9: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
consider x being set such that
A10: S9 . n = [x,(S . n)] by A5, A9;
consider y being set such that
A11: S9 . m = [y,(S . m)] by A5, A9;

then dist ((S9 . n),(S9 . m)) = dist ((S . n),(S . m)) by A10, A11, Def10;
hence not r <= dist ((S . n),(S . m)) by A6, A7, A8; :: thesis:

end;

A13: dist ((S . n),(S . m)) <= (dist ((S . n),a)) + (dist (a,(S . m))) by METRIC_1:4;
A14: dist ((S9 . n),(S9 . m)) < r by A6, A7, A8;
dist ((S9 . n),(S9 . m)) = (dist ((S . n),a)) + (dist (a,(S . m))) by A10, A11, A12, Def10;
hence not r <= dist ((S . n),(S . m)) by A13, A14, XXREAL_0:2; :: thesis:

end;

then S is convergent by A1;
then consider L being Element of M such that
A15: for r being Real st r > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
dist ((S . m),L) < r ;

take Xa ; :: according to TBSP_1:def 2 :: thesis:
A17: dist (a,a) = 0 by METRIC_1:1;
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider n being Nat such that
A18: for m being Nat st n <= m holds
dist ((S . m),L) < r by A15;
take n ; :: thesis:
let m be Nat; :: thesis:
assume A19: m >= n ; :: thesis:
A20: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
consider x being set such that
A21: S9 . m = [x,(S . m)] by A5, A20;
( x = X or x <> X ) ;
then ( dist ((S9 . m),Xa) = dist ((S . m),L) or dist ((S9 . m),Xa) = (dist ((S . m),L)) + 0 ) by A16, A21, A17, Def10;
hence dist ((S9 . m),Xa) < r by A18, A19; :: thesis:

end;

suppose A22: 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 ((S9 . m),Xa) < r ; :: thesis:

take Xa ; :: according to TBSP_1:def 2 :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider n being Nat such that
A23: for m being Nat st m >= n holds
dist ((S9 . m),Xa) < r by A22;
reconsider n = n as Nat ;
take n ; :: thesis:
let m be Nat; :: thesis:
assume m >= n ; :: thesis:
hence dist ((S9 . m),Xa) < r by A23; :: thesis:

end;

suppose A24: ( a <> L & ex n being Nat ex Y being set st
for m being Nat st m >= n holds
ex p being Point of M st S9 . m = [Y,p] ) ; :: thesis:

then consider n being Nat, Y being set such that
A25: for m being Nat st m >= n holds
ex p being Point of M st S9 . m = [Y,p] ;
A26: ex s3 being Point of M st S9 . n = [Y,s3] by A25;
A27: ex s1 being set ex s2 being Point of M st
( S9 . n = [s1,s2] & ( ( s1 in X & s2 <> a ) or ( s1 = X & s2 = a ) ) ) by Th37;

then reconsider YL = [Y,L] as Point of (WellSpace (a,X)) by A24, Th37;
take YL ; :: according to TBSP_1:def 2 :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider p being Nat such that
A28: for m being Nat st p <= m holds
dist ((S . m),L) < r by A15;
reconsider mm = max (p,n) as Nat by TARSKI:1;
take mm ; :: thesis:
let m be Nat; :: thesis:
assume A29: m >= mm ; :: thesis:
A30: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
consider x being set such that
A31: S9 . m = [x,(S . m)] by A5, A30;
mm >= n by XXREAL_0:25;
then ex pm being Point of M st S9 . m = [Y,pm] by A25, A29, XXREAL_0:2;
then x = Y by A31, XTUPLE_0:1;
then A32: dist ((S9 . m),YL) = dist ((S . m),L) by A31, Def10;
mm >= p by XXREAL_0:25;
then m >= p by A29, XXREAL_0:2;
hence dist ((S9 . m),YL) < r by A28, A32; :: thesis:

end;

reconsider n = n as Nat ;
take Xa ; :: according to TBSP_1:def 2 :: thesis:
let r be Real; :: thesis:
assume A34: r > 0 ; :: thesis:
take n ; :: thesis:
let m be Nat; :: thesis:
assume m >= n ; :: thesis:
then A35: ex t3 being Point of M st S9 . m = [Y,t3] by A25;
consider t1 being set , t2 being Point of M such that
A36: S9 . m = [t1,t2] and
A37: ( ( t1 in X & t2 <> a ) or ( t1 = X & t2 = a ) ) by Th37;
Y = t1 by A36, A35, XTUPLE_0:1;
hence dist ((S9 . m),Xa) < r by A33, A34, A36, A37, METRIC_1:1; :: thesis:

end;