for v, w being VECTOR of R_Algebra_of_Big_Oh_poly
for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds
v + w = v1 + w1