for N being Nat
for seq being Real_Sequence of N holds
( seq is non-zero iff for n being Nat holds seq . n <> 0. (TOP-REAL N) )