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

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