let k, l be Nat; :: thesis: ( k in dom (Newton_Coeff l) implies not (Newton_Coeff l) . k is zero )
assume k in dom (Newton_Coeff l) ; :: thesis: not (Newton_Coeff l) . k is zero
then A1: ( len (Newton_Coeff l) = l + 1 & len (Newton_Coeff l) >= k & k >= 1 ) by FINSEQ_3:25, NEWTON:def 5;
then reconsider i = k - 1 as Nat ;
consider m being Nat such that
A2: l + 1 = k + m by A1, NAT_1:10;
not (Newton_Coeff (m + i)) . (i + 1) is zero ;
hence not (Newton_Coeff l) . k is zero by A2; :: thesis: verum