:: deftheorem ENZ defines eventually-non-zero LIOUVIL1:def 3 :
for f being Real_Sequence holds
( f is eventually-non-zero iff for n being Nat ex N being Nat st
( n <= N & f . N <> 0 ) );