for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X)
for x being Point of (TopSpaceNorm X)
for xt being Point of (LinearTopSpaceNorm X) st S = St & x = xt holds
( St is_convergent_to xt iff S is_convergent_to x )