let f be Real_Sequence; :: thesis: ( f is eventually-nonnegative & f is eventually-nonzero implies f is eventually-positive )
assume that
A3: f is eventually-nonnegative and
A4: f is eventually-nonzero ; :: thesis: f is eventually-positive
consider N being Nat such that
A5: for n being Nat st n >= N holds
f . n >= 0 by A3;
consider M being Nat such that
A6: for n being Nat st n >= M holds
f . n <> 0 by A4;
reconsider a = max (N,M) as Nat by TARSKI:1;
take a ; :: according to ASYMPT_0:def 4 :: thesis: for n being Nat st n >= a holds
f . n > 0
let n be Nat; :: thesis: ( n >= a implies f . n > 0 )
assume A7: n >= a ; :: thesis: f . n > 0
a >= N by XXREAL_0:25;
then A8: n >= N by A7, XXREAL_0:2;
a >= M by XXREAL_0:25;
then f . n <> 0 by A6, A7, XXREAL_0:2;
hence f . n > 0 by A5, A8; :: thesis: verum