let a be Real; :: thesis: for v being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds
a * v in negligibleFuncs
let v be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: ( v in negligibleFuncs implies a * v in negligibleFuncs )
assume v in negligibleFuncs ; :: thesis: a * v in negligibleFuncs
then reconsider v1 = v as negligible Function of NAT,REAL by Def1;
a (#) v1 is negligible ;
then a * v is negligible Function of NAT,REAL by RSSPAC3;
hence a * v in negligibleFuncs by Def1; :: thesis: verum