let M be non empty MetrSpace; :: thesis: for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
let Sm be sequence of M; :: thesis: for St being sequence of (TopSpaceMetr M) st Sm = St holds
( Sm is convergent iff St is convergent )
let St be sequence of (TopSpaceMetr M); :: thesis: ( Sm = St implies ( Sm is convergent iff St is convergent ) )
assume A1: Sm = St ; :: thesis: ( Sm is convergent iff St is convergent )
thus ( Sm is convergent implies St is convergent ) :: thesis: ( St is convergent implies Sm is convergent )

proof

assume Sm is convergent ; :: thesis: St is convergent
then consider x being Point of M such that
A2: Sm is_convergent_in_metrspace_to x by METRIC_6:22;
reconsider x' = x as Point of (TopSpaceMetr M) by TOPMETR:16;
St is_convergent_to x' by A1, A2, Th31;
hence St is convergent by FRECHET:def 3; :: thesis: verum

end;

assume St is convergent ; :: thesis: Sm is convergent
then consider x' being Point of (TopSpaceMetr M) such that
A3: St is_convergent_to x' by FRECHET:def 3;
reconsider x = x' as Point of M by TOPMETR:16;
Sm is_convergent_in_metrspace_to x by A1, A3, Th31;
hence Sm is convergent by METRIC_6:21; :: thesis: verum