A7: dom g = X by FUNCT_2:def 1;
A8: dom (leq (f,g)) = (dom f) /\ (dom g) by Def5;
A9: dom f = X by FUNCT_2:def 1;
rng (leq (f,g)) c= INT ;
hence leq (f,g) is Function of X,INT by A8, A9, A7, FUNCT_2:2; :: thesis: verum