for f being Point of R_Algebra_of_Big_Oh_poly
for f1 being Point of (RAlgebra NAT)
for a being Element of REAL st f = f1 holds
a * f = a * f1