for r being Real st r in rng (Newton_Coeff n) holds
r >= 0 ;
hence Newton_Coeff n is nonnegative-yielding by PARTFUN3:def 4; :: thesis: verum