consider N being Element of NAT such that
A1: for n being Element of NAT st n >= N holds
f . n >= 0 by Def4;
consider M being Element of NAT such that
A2: for n being Element of NAT st n >= M holds
g . n >= 0 by Def4;
set a = max N,M;
f + g is eventually-nonnegative

proof

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

end;

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