for N being Nat
for seq being Real_Sequence of N holds
( seq is non-zero iff for x being set st x in NAT holds
seq . x <> 0. (TOP-REAL N) )