consider N being Nat such that
A1: for n being Nat st n >= N holds
f . n >= 0 by Def2;
c (#) f is eventually-nonnegative

proof

take N ; :: according to ASYMPT_0:def 2 :: 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 )
assume n >= N ; :: thesis: (c (#) f) . n >= 0
then f . n >= 0 by A1;
then c * (f . n) >= c * 0 ;
hence (c (#) f) . n >= 0 by SEQ_1:9; :: thesis: verum

end;

hence c (#) f is eventually-nonnegative Real_Sequence ; :: thesis: verum