let X be non empty MetrSpace; :: thesis: for x being Element of X
for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
let x be Element of X; :: thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
let S be sequence of X; :: thesis: ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )
A1: ( S is_convergent_in_metrspace_to x implies ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) )

proof

assume A2: S is_convergent_in_metrspace_to x ; :: thesis: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 )
A3: for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r )
assume A4: 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
reconsider r = r as Real ;
consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
dist ((S . n),x) < r by A2, A4;
take k = m1; :: thesis: for n being Nat st k <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r
let n be Nat; :: thesis: ( k <= n implies |.(((dist_to_point (S,x)) . n) - 0).| < r )
assume k <= n ; :: thesis: |.(((dist_to_point (S,x)) . n) - 0).| < r
then dist ((S . n),x) < r by A5;
then A6: (dist_to_point (S,x)) . n < r by Def6;
dist ((S . n),x) = (dist_to_point (S,x)) . n by Def6;
then 0 <= (dist_to_point (S,x)) . n by METRIC_1:5;
hence |.(((dist_to_point (S,x)) . n) - 0).| < r by A6, ABSVALUE:def 1; :: thesis: verum

end;

then dist_to_point (S,x) is convergent by SEQ_2:def 6;
hence ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) by A3, SEQ_2:def 7; :: thesis: verum

end;

( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 implies S is_convergent_in_metrspace_to x )

proof

assume A7: ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ; :: thesis: S is_convergent_in_metrspace_to x
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
dist ((S . n),x) < r
then consider m1 being Nat such that
A8: for n being Nat st m1 <= n holds
|.(((dist_to_point (S,x)) . n) - 0).| < r by A7, SEQ_2:def 7;
reconsider k = m1 as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: for n being Nat st k <= n holds
dist ((S . n),x) < r
let n be Nat; :: thesis: ( k <= n implies dist ((S . n),x) < r )
assume k <= n ; :: thesis: dist ((S . n),x) < r
then |.(((dist_to_point (S,x)) . n) - 0).| < r by A8;
then A9: |.(dist ((S . n),x)).| < r by Def6;
0 <= dist ((S . n),x) by METRIC_1:5;
hence dist ((S . n),x) < r by A9, ABSVALUE:def 1; :: thesis: verum

end;

hence S is_convergent_in_metrspace_to x ; :: thesis: verum

end;

hence ( S is_convergent_in_metrspace_to x iff ( dist_to_point (S,x) is convergent & lim (dist_to_point (S,x)) = 0 ) ) by A1; :: thesis: verum