for k being Nat st k in dom ((a,b) Subnomial n) holds
((a,b) Subnomial n) . k in INT by INT_1:def 2;
hence (a,b) Subnomial n is INT -valued by FINSEQ_2:12; :: thesis: verum