theorem LM16: :: ASYMPT_3:14

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