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