let f, g be Function of NAT,REAL; :: thesis: ( f is negligible & ( for x being Nat holds |.(g . x).| <= |.(f . x).| ) implies g is negligible )
assume AS: ( f is negligible & ( for x being Nat holds |.(g . x).| <= |.(f . x).| ) ) ; :: thesis: g is negligible
thus g is negligible :: thesis: verum

proof

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)
consider N being Nat such that
D3: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x) by AS;
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 N <= x ; :: thesis: |.(g . x).| < 1 / ((polynom c) . x)
then D2: |.(f . x).| < 1 / ((polynom c) . x) by D3;
|.(g . x).| <= |.(f . x).| by AS;
hence |.(g . x).| < 1 / ((polynom c) . x) by D2, XXREAL_0:2; :: thesis: verum

end;