A25:
dom g = X
by FUNCT_2:def 1;
A26:
dom (eq f,g) = (dom f) /\ (dom g)
by Def7;
A27:
dom f = X
by FUNCT_2:def 1;
rng (eq f,g) c= INT
proof
let y be
set ;
TARSKI:def 3 ( not y in rng (eq f,g) or y in INT )
assume
y in rng (eq f,g)
;
y in INT
then consider a being
set such that A28:
a in dom (eq f,g)
and A29:
y = (eq f,g) . a
by FUNCT_1:def 5;
A30:
g . a in rng g
by A26, A25, A28, FUNCT_1:12;
f . a in rng f
by A26, A27, A28, FUNCT_1:12;
then reconsider i =
f . a,
j =
g . a as
Element of
INT by A30;
thus
y in INT
by A29, INT_1:def 2;
verum
end;
hence
eq f,g is Function of X,INT
by A26, A27, A25, FUNCT_2:4; verum