theorem LM14: :: ASYMPT_3:12

for f being object holds
( f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL )