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

proof

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

end;

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