let g be polynomially-abs-bounded Function of NAT,REAL; :: thesis: ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| <= (polynom d) . x
consider k1 being Nat such that
A4: |.g.| in Big_Oh (seq_n^ k1) by defabs;
consider t1 being Element of Funcs (NAT,REAL) such that
A6: ( |.g.| = t1 & ex c1 being Real ex N1 being Element of NAT st
( c1 > 0 & ( for n being Element of NAT st n >= N1 holds
( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) ) ) ) by A4;
consider c1 being Real, N1 being Element of NAT such that
A7: ( c1 > 0 & ( for n being Element of NAT st n >= N1 holds
( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) ) ) by A6;
consider d being non empty positive-yielding XFinSequence of REAL such that
A8: for x being Nat holds c1 * (x to_power k1) <= (polynom d) . x by LRNG2;
reconsider N = N1 + 1 as Nat ;
take d ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
|.(g . x).| <= (polynom d) . x
take N ; :: thesis: for x being Nat st N <= x holds
|.(g . x).| <= (polynom d) . x
let x be Nat; :: thesis: ( N <= x implies |.(g . x).| <= (polynom d) . x )
assume B1: N <= x ; :: thesis: |.(g . x).| <= (polynom d) . x
LXN: x is Element of NAT by ORDINAL1:def 12;
N1 <= N by NAT_1:12;
then N1 <= x by XXREAL_0:2, B1;
then A9: ( t1 . x <= c1 * ((seq_n^ k1) . x) & t1 . x >= 0 ) by A7, LXN;
A10: (seq_n^ k1) . x = x to_power k1 by ASYMPT_1:def 3, LXN, B1;
c1 * (x to_power k1) <= (polynom d) . x by A8;
then t1 . x <= (polynom d) . x by A10, A9, XXREAL_0:2;
hence |.(g . x).| <= (polynom d) . x by A6, VALUED_1:18; :: thesis: verum