(Newton_Coeff ((n + 1) - 1)) null n is n + 1 -element ;
hence Newton_Coeff n is n + 1 -element ; :: thesis: verum