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
set x = lim Sm;
reconsider x9 = lim Sm as Point of (TopSpaceMetr M) by TOPMETR:12;
Sm is_convergent_in_metrspace_to lim Sm by A2, METRIC_6:12;
then ( TopSpaceMetr M is T_2 & St is_convergent_to x9 ) by A1, Th28, PCOMPS_1:34;
hence lim Sm = lim St by Th25; :: thesis: verum