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