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