let k be Nat; :: thesis: (Newton_Coeff k) . 1 = 1
((1,1) In_Power k) . 1 = 1

proof

thus ((1,1) In_Power k) . 1 = 1 |^ k by NEWTON:28
.= 1 ; :: thesis: verum

end;

hence (Newton_Coeff k) . 1 = 1 by NEWTON:31; :: thesis: verum