let p be Real_Sequence; :: thesis: ( p is polynomially-bounded implies p is polynomially-abs-bounded )
assume p is polynomially-bounded ; :: thesis: p is polynomially-abs-bounded
then consider k being Nat such that
L1: p in Big_Oh (seq_n^ k) ;
consider t being Element of Funcs (NAT,REAL) such that
L2: ( p = t & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * ((seq_n^ k) . n) & t . n >= 0 ) ) ) ) by L1;
consider c being Real, N being Element of NAT such that
L3: ( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * ((seq_n^ k) . n) & t . n >= 0 ) ) ) by L2;
reconsider abst = |.t.| as Element of Funcs (NAT,REAL) by FUNCT_2:8;
for n being Element of NAT st n >= N holds
( abst . n <= c * ((seq_n^ k) . n) & abst . n >= 0 )

proof

let n be Element of NAT ; :: thesis: ( n >= N implies ( abst . n <= c * ((seq_n^ k) . n) & abst . n >= 0 ) )
assume LL2: n >= N ; :: thesis: ( abst . n <= c * ((seq_n^ k) . n) & abst . n >= 0 )
then t . n = |.(t . n).| by ABSVALUE:def 1, L3
.= |.t.| . n by VALUED_1:18 ;
hence ( abst . n <= c * ((seq_n^ k) . n) & abst . n >= 0 ) by LL2, L3; :: thesis: verum

end;

then |.p.| in Big_Oh (seq_n^ k) by L2, L3;
hence p is polynomially-abs-bounded ; :: thesis: verum