( (k + 1) + l >= (k + 1) + 0 & k + 1 >= 0 + 1 ) by XREAL_1:6;
then ( len (Newton_Coeff (l + k)) >= k + 1 & k + 1 >= 1 ) by NEWTON:def 5;
then k + 1 in dom (Newton_Coeff (l + k)) by FINSEQ_3:25;
then (Newton_Coeff (l + k)) . (k + 1) = (l + k) choose ((k + 1) - 1) by NEWTON:def 5;
hence (Newton_Coeff (l + k)) . (k + 1) is positive ; :: thesis: verum