A5: dom g = X by FUNCT_2:def 1;
A6: dom (f mod g) = (dom f) /\ (dom g) by Def4;
A7: dom f = X by 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
a in dom (f mod g) and
A8: y = (f mod g) . a by FUNCT_1:def 3;
thus y in INT by A8, INT_1:def 2; :: thesis: verum

end;

hence f mod g is Function of X,INT by A6, A7, A5, FUNCT_2:2; :: thesis: verum