theorem Th7: :: NDIFF_1:7

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 )