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

(Newton_Coeff n) . k in NAT by ORDINAL1:def 12;

hence Newton_Coeff n is NAT -valued by FINSEQ_2:12; :: thesis: verum

(Newton_Coeff n) . k in NAT by ORDINAL1:def 12;

hence Newton_Coeff n is NAT -valued by FINSEQ_2:12; :: thesis: verum