let M be non empty MetrSpace; :: thesis:
let S be sequence of M; :: thesis:
let x be Point of M; :: thesis:
let S9 be sequence of (TopSpaceMetr M); :: thesis:
let x9 be Point of (TopSpaceMetr M); :: thesis:
assume that
A1: S = S9 and
A2: x = x9 ; :: thesis:
thus ( S is_convergent_in_metrspace_to x implies S9 is_convergent_to x9 ) :: thesis:

proof

assume A3: S is_convergent_in_metrspace_to x ; :: thesis:
let U1 be Subset of (TopSpaceMetr M); :: according to FRECHET:def 3 :: thesis:
assume ( U1 is open & x9 in U1 ) ; :: thesis:
then consider r being Real such that
A4: r > 0 and
A5: Ball (x,r) c= U1 by A2, TOPMETR:15;
reconsider r = r as Real ;
Ball (x,r) contains_almost_all_sequence S by A3, A4, METRIC_6:15;
then consider n being Nat such that
A6: for m being Nat st n <= m holds
S . m in Ball (x,r) ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then S . m in Ball (x,r) by A6;
hence S9 . m in U1 by A1, A5; :: thesis:

end;

assume A7: S9 is_convergent_to x9 ; :: thesis:
for V being Subset of M st x in V & V in Family_open_set M holds
V contains_almost_all_sequence S

proof

let V be Subset of M; :: thesis:
assume that
A8: x in V and
A9: V in Family_open_set M ; :: thesis:
reconsider V9 = V as Subset of (TopSpaceMetr M) by TOPMETR:12;
reconsider V9 = V9 as Subset of (TopSpaceMetr M) ;
V9 in the topology of (TopSpaceMetr M) by A9, TOPMETR:12;
then V9 is open ;
then consider n being Nat such that
A10: for m being Nat st n <= m holds
S9 . m in V9 by A2, A7, A8;
take n ; :: according to METRIC_6:def 5 :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
hence S . m in V by A1, A10; :: thesis:

end;

hence S is_convergent_in_metrspace_to x by METRIC_6:17; :: thesis: