consider M being Nat such that
A1: for n being Nat st n >= M holds
g . n >= 0 by Def2;
consider N being Nat such that
A2: for n being Nat st n >= N holds
f . n >= 0 by Def2;
reconsider a = max (N,M) as Nat by TARSKI:1;
f + g is eventually-nonnegative

proof

take a ; :: according to ASYMPT_0:def 2 :: thesis: for n being Nat st n >= a holds
(f + g) . n >= 0
let n be Nat; :: thesis: ( n >= a implies (f + g) . n >= 0 )
assume A3: n >= a ; :: thesis: (f + g) . n >= 0
a >= M by XXREAL_0:25;
then n >= M by A3, XXREAL_0:2;
then A4: g . n >= 0 by A1;
a >= N by XXREAL_0:25;
then n >= N by A3, XXREAL_0:2;
then f . n >= 0 by A2;
then 0 + 0 <= (f . n) + (g . n) by A4;
hence (f + g) . n >= 0 by SEQ_1:7; :: thesis: verum

end;

hence f + g is eventually-nonnegative Real_Sequence ; :: thesis: verum