A1: ( rng f c= INT & rng g c= INT & dom (f mod g) = (dom f) /\ (dom g) & (dom f) /\ (dom f) = dom f & dom f = X & dom g = X ) by DEFmod, FUNCT_2:def 1;
rng (f mod g) c= INT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (f mod g) or y in INT )
assume y in rng (f mod g) ; :: thesis: y in INT
then consider a being set such that
A2: ( a in dom (f mod g) & y = (f mod g) . a ) by FUNCT_1:def 5;
( f . a in rng f & g . a in rng g ) by A1, A2, FUNCT_1:12;
then reconsider i = f . a, j = g . a as Element of INT ;
thus y in INT by A2, INT_1:def 2; :: thesis: verum

end;

hence f mod g is Function of X,INT by A1, FUNCT_2:4; :: thesis: verum