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 number st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point S,x) . n) - 0 ) < r

proof

let r be real number ; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point S,x) . n) - 0 ) < r )
assume A4: 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
abs (((dist_to_point S,x) . n) - 0 ) < r
reconsider r = r as Real by XREAL_0:def 1;
consider m1 being Element of NAT such that
A5: for n being Element of NAT st m1 <= n holds
dist (S . n),x < r by A2, A4, Def8;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
abs (((dist_to_point S,x) . n) - 0 ) < r
let n be Element of NAT ; :: thesis: ( k <= n implies abs (((dist_to_point S,x) . n) - 0 ) < r )
assume k <= n ; :: thesis: abs (((dist_to_point S,x) . n) - 0 ) < r
then A6: dist (S . n),x < r by A5;
A7: dist (S . n),x = (dist_to_point S,x) . n by Def14;
A8: (dist_to_point S,x) . n < r by A6, Def14;
0 <= (dist_to_point S,x) . n by A7, METRIC_1:5;
hence abs (((dist_to_point S,x) . n) - 0 ) < r by A8, 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 A9: ( 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 Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r )
assume 0 < r ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
dist (S . n),x < r
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st m1 <= n holds
abs (((dist_to_point S,x) . n) - 0 ) < r by A9, SEQ_2:def 7;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
dist (S . n),x < r
let n be Element of NAT ; :: thesis: ( k <= n implies dist (S . n),x < r )
assume k <= n ; :: thesis: dist (S . n),x < r
then abs (((dist_to_point S,x) . n) - 0 ) < r by A10;
then A11: abs (dist (S . n),x) < r by Def14;
0 <= dist (S . n),x by METRIC_1:5;
hence dist (S . n),x < r by A11, ABSVALUE:def 1; :: thesis: verum

end;

hence S is_convergent_in_metrspace_to x by Def8; :: 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