the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;
hence the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of (RAlgebra NAT) ; :: thesis: verum