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

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;

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

hence (Newton_Coeff n) . m is natural by FUNCT_1:def 2; :: thesis: verum

end;

end;