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 Nat such that
A2: for n being Nat st n >= N holds
f . n > 0 ;
thus f is eventually-nonnegative :: thesis: f is eventually-nonzero
proof
take N ; :: according to ASYMPT_0:def 2 :: thesis: for n being Nat st n >= N holds
f . n >= 0
let n be 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 5 :: thesis: for n being Nat st n >= N holds
f . n <> 0
let n be Nat; :: thesis: ( n >= N implies f . n <> 0 )
assume n >= N ; :: thesis: f . n <> 0
hence f . n <> 0 by A2; :: thesis: verum
end;