for X being RealNormSpace
for S being sequence of (TopSpaceNorm X)
for St being sequence of (LinearTopSpaceNorm X) st S = St holds
( St is convergent iff S is convergent )