A13:
dom g = X
by FUNCT_2:def 1;
A14:
dom (leq f,g) = (dom f) /\ (dom g)
by Def5;
A15:
dom f = X
by FUNCT_2:def 1;
rng (leq f,g) c= INT
proof
let y be
set ;
TARSKI:def 3 ( not y in rng (leq f,g) or y in INT )
assume
y in rng (leq f,g)
;
y in INT
then consider a being
set such that A16:
a in dom (leq f,g)
and A17:
y = (leq f,g) . a
by FUNCT_1:def 5;
A18:
g . a in rng g
by A14, A13, A16, FUNCT_1:12;
f . a in rng f
by A14, A15, A16, FUNCT_1:12;
then reconsider i =
f . a,
j =
g . a as
Element of
INT by A18;
thus
y in INT
by A17, INT_1:def 2;
verum
end;
hence
leq f,g is Function of X,INT
by A14, A15, A13, FUNCT_2:4; verum