for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for n being Nat holds seq . n <> 0. S )