let g be Function of NAT,REAL; :: thesis: ( g = a (#) f implies g is negligible )
assume A1: g = a (#) f ; :: thesis: g 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
|.(g . x).| < 1 / ((polynom c) . x)

per cases ( a = 0 or a <> 0 ) ;

suppose D1: a = 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom c) . x)

take N = 0 ; :: thesis: for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom c) . x)
let x be Nat; :: thesis: ( N <= x implies |.(g . x).| < 1 / ((polynom c) . x) )
assume N <= x ; :: thesis: |.(g . x).| < 1 / ((polynom c) . x)
D2: |.((a (#) f) . x).| = |.(a * (f . x)).| by VALUED_1:6
.= 0 by D1 ;
0 < (polynom c) . x by NLM3;
hence |.(g . x).| < 1 / ((polynom c) . x) by A1, D2; :: thesis: verum

end;

suppose F1: a <> 0 ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom c) . x)

reconsider c1 = |.a.| (#) c as non empty positive-yielding XFinSequence of REAL by F1;
consider N being Nat such that
F3: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c1) . x) by defneg;
take N ; :: thesis: for x being Nat st N <= x holds
|.(g . x).| < 1 / ((polynom c) . x)
let x be Nat; :: thesis: ( N <= x implies |.(g . x).| < 1 / ((polynom c) . x) )
assume F4: N <= x ; :: thesis: |.(g . x).| < 1 / ((polynom c) . x)
K2: 0 < (polynom c) . x by NLM3;
F6: (polynom c1) . x = |.a.| * ((polynom c) . x) by NLM4;
K4: 0 < (polynom c1) . x by NLM3;
|.(f . x).| < 1 / ((polynom c1) . x) by F3, F4;
then |.(f . x).| * ((polynom c1) . x) < (1 / ((polynom c1) . x)) * ((polynom c1) . x) by K4, XREAL_1:68;
then (|.(f . x).| * |.a.|) * ((polynom c) . x) < 1 by F6, K4, XCMPLX_1:87;
then |.(a * (f . x)).| * ((polynom c) . x) < 1 by COMPLEX1:65;
then |.((a (#) f) . x).| * ((polynom c) . x) < 1 by VALUED_1:6;
then (|.((a (#) f) . x).| * ((polynom c) . x)) / ((polynom c) . x) < 1 / ((polynom c) . x) by K2, XREAL_1:74;
hence |.(g . x).| < 1 / ((polynom c) . x) by A1, K2, XCMPLX_1:89; :: thesis: verum

end;

end;