for X being RealNormSpace
for S being sequence of X
for St being sequence of (MetricSpaceNorm X) st S = St & St is convergent holds
lim St = lim S