A4: dom g = X by FUNCT_2:def 1;
A5: dom (f mod g) = (dom f) /\ (dom g) by Def4;
A6: dom f = X by FUNCT_2:def 1;
rng (f mod g) c= INT ;
hence f mod g is Function of X,INT by A5, A6, A4, FUNCT_2:2; :: thesis: verum