let h be Function of NAT,REAL; :: thesis: ( h = f + g implies h is negligible )
assume A0: h = f + g ; :: thesis: h is negligible
let c be non empty positive-yielding XFinSequence of REAL ; :: according to ASYMPT_3:def 4 :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(h . x).| < 1 / ((polynom c) . x)
reconsider c1 = 2 (#) c as non empty positive-yielding XFinSequence of REAL ;
consider N1 being Nat such that
D1: for x being Nat st N1 <= x holds
|.(f . x).| < 1 / ((polynom c1) . x) by defneg;
consider N2 being Nat such that
D2: for x being Nat st N2 <= x holds
|.(g . x).| < 1 / ((polynom c1) . x) by defneg;
take N = N1 + N2; :: thesis: for x being Nat st N <= x holds
|.(h . x).| < 1 / ((polynom c) . x)
let x be Nat; :: thesis: ( N <= x implies |.(h . x).| < 1 / ((polynom c) . x) )
assume D3: N <= x ; :: thesis: |.(h . x).| < 1 / ((polynom c) . x)
N1 <= N by NAT_1:12;
then N1 <= x by D3, XXREAL_0:2;
then D4: |.(f . x).| < 1 / ((polynom c1) . x) by D1;
N2 <= N by NAT_1:12;
then N2 <= x by D3, XXREAL_0:2;
then D5: |.(g . x).| < 1 / ((polynom c1) . x) by D2;
F6: (polynom c1) . x = 2 * ((polynom c) . x) by NLM4;
|.((f + g) . x).| = |.((f . x) + (g . x)).|

proof

x in NAT by ORDINAL1:def 12;
hence |.((f + g) . x).| = |.((f . x) + (g . x)).| by VALUED_1:1; :: thesis: verum

end;

then D6: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by COMPLEX1:56;
|.(f . x).| + |.(g . x).| < (1 / ((polynom c1) . x)) + (1 / ((polynom c1) . x)) by D4, D5, XREAL_1:8;
then |.((f + g) . x).| < 2 * (1 / ((polynom c1) . x)) by XXREAL_0:2, D6;
hence |.(h . x).| < 1 / ((polynom c) . x) by A0, XCMPLX_1:92, F6; :: thesis: verum