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:10;
reconsider x9 = x as Point of (TopSpaceMetr M) by TOPMETR:12;
St is_convergent_to x9 by A1, A2, Th28;
hence St is convergent ; :: thesis: verum
end;
assume St is convergent ; :: thesis: Sm is convergent
then consider x9 being Point of (TopSpaceMetr M) such that
A3: St is_convergent_to x9 ;
reconsider x = x9 as Point of M by TOPMETR:12;
Sm is_convergent_in_metrspace_to x by A1, A3, Th28;
hence Sm is convergent by METRIC_6:9; :: thesis: verum