let M be non empty MetrSpace; :: thesis: for Sm being sequence of M
for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St
let Sm be sequence of M; :: thesis: for St being sequence of (TopSpaceMetr M) st Sm = St & Sm is convergent holds
lim Sm = lim St
let St be sequence of (TopSpaceMetr M); :: thesis: ( Sm = St & Sm is convergent implies lim Sm = lim St )
assume that
A1: Sm = St and
A2: Sm is convergent ; :: thesis: lim Sm = lim St
A3: TopSpaceMetr M is T_2 by PCOMPS_1:38;
set x = lim Sm;
reconsider x' = lim Sm as Point of (TopSpaceMetr M) by TOPMETR:16;
Sm is_convergent_in_metrspace_to lim Sm by A2, METRIC_6:27;
then St is_convergent_to x' by A1, Th31;
hence lim Sm = lim St by A3, Th28; :: thesis: verum