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 Th38;
assume A1: M is complete ; :: thesis:
let S9 be sequence of (WellSpace a,X); :: according to TBSP_1:def 6 :: thesis:
assume A2: S9 is Cauchy ; :: thesis:
defpred S₁[ set , set ] means ex x being set st S9 . $1 = [x,$2];
A3: for x being set st x in NAT holds
ex y being set st
( y in the carrier of M & S₁[x,y] )

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider i = x as Element of 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 Th38;
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 set 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 5 :: thesis:
assume r > 0 ; :: thesis:
then consider p being Element of NAT such that
A6: for n, m being Element of NAT st p <= n & p <= m holds
dist (S9 . n),(S9 . m) < r by A2, TBSP_1:def 5;
take p ; :: thesis:
let n, m be Element of NAT ; :: thesis:
assume that
A7: p <= n and
A8: p <= m ; :: thesis:
consider x being set such that
A9: S9 . n = [x,(S . n)] by A5;
consider y being set such that
A10: S9 . m = [y,(S . m)] by A5;

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

end;

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

end;

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

take Xa ; :: according to TBSP_1:def 3 :: thesis:
A16: dist a,a = 0 by METRIC_1:1;
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider n being Element of NAT such that
A17: for m being Element of NAT st n <= m holds
dist (S . m),L < r by A14;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A18: m >= n ; :: thesis:
consider x being set such that
A19: S9 . m = [x,(S . m)] by A5;
( 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 A15, A19, A16, Def10;
hence dist (S9 . m),Xa < r by A17, A18; :: thesis:

end;

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

take Xa ; :: according to TBSP_1:def 3 :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider n being natural number such that
A21: for m being natural number st m >= n holds
dist (S9 . m),Xa < r by A20;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume m >= n ; :: thesis:
hence dist (S9 . m),Xa < r by A21; :: thesis:

end;

suppose A22: ( a <> L & 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 S9 . m = [Y,p] ) ; :: thesis:

then consider n being natural number , Y being set such that
A23: for m being natural number st m >= n holds
ex p being Point of M st S9 . m = [Y,p] ;
A24: ex s3 being Point of M st S9 . n = [Y,s3] by A23;
A25: 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 Th38;

then reconsider YL = [Y,L] as Point of (WellSpace a,X) by A22, Th38;
take YL ; :: according to TBSP_1:def 3 :: thesis:
let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider p being Element of NAT such that
A26: for m being Element of NAT st p <= m holds
dist (S . m),L < r by A14;
reconsider mm = max p,n as Element of NAT by ORDINAL1:def 13;
take mm ; :: thesis:
let m be Element of NAT ; :: thesis:
assume A27: m >= mm ; :: thesis:
consider x being set such that
A28: S9 . m = [x,(S . m)] by A5;
mm >= n by XXREAL_0:25;
then ex pm being Point of M st S9 . m = [Y,pm] by A23, A27, XXREAL_0:2;
then x = Y by A28, ZFMISC_1:33;
then A29: dist (S9 . m),YL = dist (S . m),L by A28, Def10;
mm >= p by XXREAL_0:25;
then m >= p by A27, XXREAL_0:2;
hence dist (S9 . m),YL < r by A26, A29; :: thesis:

end;

reconsider n = n as Element of NAT by ORDINAL1:def 13;
take Xa ; :: according to TBSP_1:def 3 :: thesis:
let r be Real; :: thesis:
assume A31: r > 0 ; :: thesis:
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
assume m >= n ; :: thesis:
then A32: ex t3 being Point of M st S9 . m = [Y,t3] by A23;
consider t1 being set , t2 being Point of M such that
A33: S9 . m = [t1,t2] and
A34: ( ( t1 in X & t2 <> a ) or ( t1 = X & t2 = a ) ) by Th38;
Y = t1 by A33, A32, ZFMISC_1:33;
hence dist (S9 . m),Xa < r by A30, A31, A33, A34, METRIC_1:1; :: thesis:

end;