let n be Nat; :: thesis: Newton_Coeff n is FinSequence of NAT

for k being Nat st k in dom (Newton_Coeff n) holds

(Newton_Coeff n) . k in NAT ;

hence Newton_Coeff n is FinSequence of NAT by FINSEQ_2:12; :: thesis: verum

for k being Nat st k in dom (Newton_Coeff n) holds

(Newton_Coeff n) . k in NAT ;

hence Newton_Coeff n is FinSequence of NAT by FINSEQ_2:12; :: thesis: verum