theorem LM12: :: ASYMPT_3:11

the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of (RAlgebra NAT)