theorem :: NORMSP_2:11

for X being RealNormSpace holds TopSpaceNorm X is sequential ;