:: deftheorem Def5 defines eventually-nonzero ASYMPT_0:def 5 :
for f being Real_Sequence holds
( f is eventually-nonzero iff ex N being Nat st
for n being Nat st n >= N holds
f . n <> 0 );