( n + 1 >= n + 0 & n >= 1 ) by NAT_1:14, XREAL_1:6;
then ( len (Newton_Coeff n) >= n & n >= 1 ) by NEWTON:def 5;
then n in dom (Newton_Coeff n) by FINSEQ_3:25;
then (Newton_Coeff n) . n = n choose (n - 1) by NEWTON:def 5;
hence (Newton_Coeff n) . n = n by NEWTON:24, NAT_1:14; :: thesis: verum