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