let h be Function of NAT,REAL; :: thesis: ( h = g (#) f implies h is negligible )
assume A0: h = g (#) f ; :: thesis: h is negligible
consider s being non empty positive-yielding XFinSequence of REAL , N0 being Nat such that
P1: for x being Nat st N0 <= x holds
|.(g . x).| <= (polynom s) . x by RNG2;
let d 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 d) . x)
(polynom s) (#) f is negligible ;
then consider N1 being Nat such that
P2: for x being Nat st N1 <= x holds
|.(((polynom s) (#) f) . x).| < 1 / ((polynom d) . x) ;
take N = N1 + N0; :: thesis: for x being Nat st N <= x holds
|.(h . x).| < 1 / ((polynom d) . x)
let x be Nat; :: thesis: ( N <= x implies |.(h . x).| < 1 / ((polynom d) . x) )
assume P3: N <= x ; :: thesis: |.(h . x).| < 1 / ((polynom d) . x)
P4: |.((g (#) f) . x).| = |.((g . x) * (f . x)).| by VALUED_1:5
.= |.(g . x).| * |.(f . x).| by COMPLEX1:65 ;
N0 <= N by NAT_1:12;
then N0 <= x by XXREAL_0:2, P3;
then P6: |.(g . x).| <= (polynom s) . x by P1;
Q7: 0 < (polynom s) . x by NLM3;
((polynom s) . x) * |.(f . x).| = |.((polynom s) . x).| * |.(f . x).| by Q7, ABSVALUE:def 1
.= |.(((polynom s) . x) * (f . x)).| by COMPLEX1:65
.= |.(((polynom s) (#) f) . x).| by VALUED_1:5 ;
then P8: |.((g (#) f) . x).| <= |.(((polynom s) (#) f) . x).| by P4, XREAL_1:66, P6;
N1 <= N by NAT_1:12;
then N1 <= x by P3, XXREAL_0:2;
then |.(((polynom s) (#) f) . x).| < 1 / ((polynom d) . x) by P2;
hence |.(h . x).| < 1 / ((polynom d) . x) by A0, P8, XXREAL_0:2; :: thesis: verum