len
(
Newton_Coeff
n
)
=
n
+
1
by
NEWTON:def 5
;
hence
not
Newton_Coeff
n
is
empty
;
:: thesis:
verum