for a being Real
for v being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds
a * v in negligibleFuncs