for S being RealNormSpace
for seq being sequence of S holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. S )