let v, u be VECTOR of R_Algebra_of_Big_Oh_poly; :: thesis: ( v in negligibleFuncs & u in negligibleFuncs implies v * u in negligibleFuncs )
assume ( v in negligibleFuncs & u in negligibleFuncs ) ; :: thesis: v * u in negligibleFuncs
then reconsider v1 = v, u1 = u as negligible Function of NAT,REAL by Def1;
v1 (#) u1 is negligible ;
then v * u is negligible Function of NAT,REAL by RSSPAC2A;
hence v * u in negligibleFuncs by Def1; :: thesis: verum