for f, g being Point of R_Algebra_of_Big_Oh_poly
for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds
f * g = f1 * g1