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 RSSPAC2;
hence v + u in negligibleFuncs by Def1; :: thesis: verum