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