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 ( S is convergent & lim S = x ) )
let x be Element of X; :: thesis: for S being sequence of X holds
( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
let S be sequence of X; :: thesis: ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) )
( S is convergent & lim S = x implies S is_convergent_in_metrspace_to x )

proof

assume ( S is convergent & lim S = x ) ; :: thesis: S is_convergent_in_metrspace_to x
then 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 by TBSP_1:def 4;
hence S is_convergent_in_metrspace_to x by Def8; :: thesis: verum

end;

hence ( S is_convergent_in_metrspace_to x iff ( S is convergent & lim S = x ) ) by Th21, Th26; :: thesis: verum