A1: dom g = X by FUNCT_2:def 1;
A2: dom (f div g) = (dom f) /\ (dom g) by Def3;
A3: dom f = X by FUNCT_2:def 1;
rng (f div g) c= INT ;
hence f div g is Function of X,INT by A2, A3, A1, FUNCT_2:2; :: thesis: verum