:: 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 );

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 );