:: deftheorem defAlgebra defines R_Algebra_of_Big_Oh_poly ASYMPT_3:def 3 :
for b₁ being strict AlgebraStr holds
( b₁ = R_Algebra_of_Big_Oh_poly iff ( the carrier of b₁ = Big_Oh_poly & the multF of b₁ = (RealFuncMult NAT) || Big_Oh_poly & the addF of b₁ = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b₁ = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b₁ = RealFuncUnit NAT & the ZeroF of b₁ = RealFuncZero NAT ) );