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 dist ((S . n),x) < r by A5;
then A6: (dist_to_point (S,x)) . n < r by Def14;
dist ((S . n),x) = (dist_to_point (S,x)) . n by Def14;
then 0 <= (dist_to_point (S,x)) . n by METRIC_1:5;
hence abs (((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 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
A8: for n being Element of NAT st m1 <= n holds
abs (((dist_to_point (S,x)) . n) - 0) < r by A7, 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 A8;
then A9: abs (dist ((S . n),x)) < r by Def14;
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 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