let n be Nat; :: thesis: (Newton_Coeff n) . (n + 1) = 1
A1: len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
then A2: n = (len (Newton_Coeff n)) - 1 ;
n + 1 in dom (Newton_Coeff n) by A1, Th3;
then (Newton_Coeff n) . (n + 1) = n choose n by A2, NEWTON:def 5;
hence (Newton_Coeff n) . (n + 1) = 1 by NEWTON:21; :: thesis: verum