per cases
( m in dom (Newton_Coeff n) or not m in dom (Newton_Coeff n) )
;

end;

suppose A0:
m in dom (Newton_Coeff n)
; :: thesis: (Newton_Coeff n) . m is natural

then consider k being Nat such that

A1: m = 1 + k by NAT_1:10, FINSEQ_3:25;

k = m - 1 by A1;

then (Newton_Coeff n) . m = n choose k by A0, NEWTON:def 5;

hence (Newton_Coeff n) . m is natural ; :: thesis: verum

end;A1: m = 1 + k by NAT_1:10, FINSEQ_3:25;

k = m - 1 by A1;

then (Newton_Coeff n) . m = n choose k by A0, NEWTON:def 5;

hence (Newton_Coeff n) . m is natural ; :: thesis: verum