for v, u being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds
v + u in negligibleFuncs