A9: dom g = X by FUNCT_2:def 1;
A10: dom (leq (f,g)) = (dom f) /\ (dom g) by Def5;
A11: dom f = X by FUNCT_2:def 1;
rng (leq (f,g)) c= INT

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (leq (f,g)) or y in INT )
assume y in rng (leq (f,g)) ; :: thesis: y in INT
then consider a being set such that
a in dom (leq (f,g)) and
A12: y = (leq (f,g)) . a by FUNCT_1:def 3;
thus y in INT by A12, INT_1:def 2; :: thesis: verum

end;

hence leq (f,g) is Function of X,INT by A10, A11, A9, FUNCT_2:2; :: thesis: verum