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