let n be Nat; :: thesis: len ((Newton_Coeff n) | n) = n
len (Newton_Coeff n) = n + 1 by NEWTON:def 5;
then n < len (Newton_Coeff n) by NAT_1:13;
hence len ((Newton_Coeff n) | n) = n by FINSEQ_1:59; :: thesis: verum