consider N being Nat such that
A1: for n being Nat st n >= N holds
f . n >= 0 by Def2;
c + f is eventually-positive
proof
take N ; :: according to ASYMPT_0:def 4 :: thesis: for n being Nat st n >= N holds
(c + f) . n > 0
let n be Nat; :: thesis: ( n >= N implies (c + f) . n > 0 )
A2: n in NAT by ORDINAL1:def 12;
assume n >= N ; :: thesis: (c + f) . n > 0
then f . n >= 0 by A1;
then c + (f . n) > 0 + 0 ;
hence (c + f) . n > 0 by VALUED_1:2, A2; :: thesis: verum
end;
hence c + f is eventually-positive Real_Sequence ; :: thesis: verum