let n be Nat; :: thesis: ( n > 0 implies n in dom (Newton_Coeff n) )
assume n > 0 ; :: thesis: n in dom (Newton_Coeff n)
then A1: n in Seg n by FINSEQ_1:3;
dom (Newton_Coeff n) = Seg (len (Newton_Coeff n)) by FINSEQ_1:def 3
.= Seg (n + 1) by NEWTON:def 5 ;
hence n in dom (Newton_Coeff n) by A1, FINSEQ_2:8; :: thesis: verum