for X being RealNormSpace holds TopSpaceNorm X is sequential ;