:: deftheorem defines non-zero TOPRNS_1:def 1 :
for N being Nat
for IT being Real_Sequence of N holds
( IT is non-zero iff rng IT c= NonZero (TOP-REAL N) );