len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
hence not Newton_Coeff n is empty ; :: thesis: verum