let f be Real_Sequence; :: thesis: ( f is eventually-positive implies ( f is eventually-nonnegative & f is eventually-nonzero ) )
assume f is eventually-positive ; :: thesis: ( f is eventually-nonnegative & f is eventually-nonzero )
then consider N being Element of NAT such that
A2: for n being Element of NAT st n >= N holds
f . n > 0 by Def6;
thus f is eventually-nonnegative :: thesis: f is eventually-nonzero

proof

take N ; :: according to ASYMPT_0:def 4 :: thesis: for n being Element of NAT st n >= N holds
f . n >= 0
let n be Element of NAT ; :: thesis: ( n >= N implies f . n >= 0 )
assume n >= N ; :: thesis: f . n >= 0
hence f . n >= 0 by A2; :: thesis: verum

end;

thus f is eventually-nonzero :: thesis: verum

proof

take N ; :: according to ASYMPT_0:def 7 :: thesis: for n being Element of NAT st n >= N holds
f . n <> 0
let n be Element of NAT ; :: thesis: ( n >= N implies f . n <> 0 )
assume n >= N ; :: thesis: f . n <> 0
hence f . n <> 0 by A2; :: thesis: verum

end;