for f, g, h being VECTOR of R_Algebra_of_Big_Oh_poly
for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds
( h = f + g iff for x being Nat holds h9 . x = (f9 . x) + (g9 . x) )