let f be object ; :: thesis: ( f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL )
the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;
hence ( f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL ) by DefX1; :: thesis: verum