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