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

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