let v, w be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: ( w in negligibleFuncs implies v * w in negligibleFuncs )
assume w in negligibleFuncs ; :: thesis: v * w in negligibleFuncs
then reconsider w1 = w as negligible Function of NAT,REAL by Def1;
v in R_Algebra_of_Big_Oh_poly ;
then reconsider v1 = v as polynomially-abs-bounded Function of NAT,REAL by LM14;
v1 (#) w1 is negligible ;
then v * w is negligible Function of NAT,REAL by RSSPAC2A;
hence v * w in negligibleFuncs by Def1; :: thesis: verum