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

then (Newton_Coeff n) . m divides ((a,b) In_Power n) . m by NIS;
then consider x being Integer such that
A2: ((a,b) In_Power n) . m = ((Newton_Coeff n) . m) * x ;
(Newton_Coeff n) . m <> 0 by A0, D1;
then x = (((a,b) In_Power n) . m) / ((Newton_Coeff n) . m) by A2, XCMPLX_1:89;
hence ((a,b) Subnomial n) . m is integer by VALUED_1:17; :: thesis:

end;

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

then (Newton_Coeff n) . m = 0 by FUNCT_1:def 2;
then 0 = (((a,b) In_Power n) . m) / ((Newton_Coeff n) . m) by XCMPLX_1:49;
hence ((a,b) Subnomial n) . m is integer by VALUED_1:17; :: thesis:

end;

end;