let f be Function of NAT,REAL; :: thesis: ( f is negligible implies f is polynomially-abs-bounded )
assume A0: f is negligible ; :: thesis: f is polynomially-abs-bounded
consider c being non empty positive-yielding XFinSequence of REAL such that
P1: for x being Nat holds (polynom c) . x = 1 by PXR1;
consider N being Nat such that
P2: for x being Nat st N <= x holds
|.(f . x).| < 1 / ((polynom c) . x) by A0;
set s = |.f.|;
ZP1: |.f.| in Funcs (NAT,REAL) by FUNCT_2:8;

now :: thesis: for n being Element of NAT st n >= N + 2 holds
( |.f.| . n <= 1 * ((seq_n^ 1) . n) & |.f.| . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= N + 2 implies ( |.f.| . n <= 1 * ((seq_n^ 1) . n) & |.f.| . n >= 0 ) )
assume A2: n >= N + 2 ; :: thesis: ( |.f.| . n <= 1 * ((seq_n^ 1) . n) & |.f.| . n >= 0 )
2 <= N + 2 by NAT_1:12;
then 2 <= n by A2, XXREAL_0:2;
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ 1) . n = n to_power 1 by A2, ASYMPT_1:def 3
.= n ;
A5: |.f.| . n = |.(f . n).| by VALUED_1:18;
N <= N + 2 by NAT_1:12;
then N <= n by A2, XXREAL_0:2;
then |.f.| . n < 1 / ((polynom c) . n) by A5, P2;
then |.f.| . n < 1 / 1 by P1;
hence |.f.| . n <= 1 * ((seq_n^ 1) . n) by XXREAL_0:2, A3, A4; :: thesis: |.f.| . n >= 0
thus |.f.| . n >= 0 by A5; :: thesis: verum

end;

then |.f.| in Big_Oh (seq_n^ 1) by ZP1;
hence f is polynomially-abs-bounded ; :: thesis: verum