let g be Function of NAT,REAL; :: thesis: ( g = |.f.| implies g is negligible )
assume A1: g = |.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)
consider N being Nat such that
D3: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . 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 B1: N <= x ; :: thesis: |.(g . x).| < 1 / ((polynom c) . x)
|.(|.f.| . x).| = |.|.(f . x).|.| by SEQ_1:12
.= |.(f . x).| ;
hence |.(g . x).| < 1 / ((polynom c) . x) by A1, D3, B1; :: thesis: verum