for S being RealNormSpace
for a being non-zero 0 -convergent Real_Sequence
for z being Point of S st z <> 0. S holds
( a * z is non-zero & a * z is 0. S -convergent )