(Newton_Coeff n) . (n + 1) = ((1,1) In_Power n) . (n + 1) by NEWTON:31
.= 1 |^ n by NEWTON:29 ;
hence (Newton_Coeff n) . (n + 1) = 1 ; :: thesis: verum