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

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