A19:
dom g = X
by FUNCT_2:def 1;
A20:
dom (gt f,g) = (dom f) /\ (dom g)
by Def6;
A21:
dom f = X
by FUNCT_2:def 1;
rng (gt f,g) c= INT
proof
let y be
set ;
TARSKI:def 3 ( not y in rng (gt f,g) or y in INT )
assume
y in rng (gt f,g)
;
y in INT
then consider a being
set such that A22:
a in dom (gt f,g)
and A23:
y = (gt f,g) . a
by FUNCT_1:def 5;
A24:
g . a in rng g
by A20, A19, A22, FUNCT_1:12;
f . a in rng f
by A20, A21, A22, FUNCT_1:12;
then reconsider i =
f . a,
j =
g . a as
Element of
INT by A24;
thus
y in INT
by A23, INT_1:def 2;
verum
end;
hence
gt f,g is Function of X,INT
by A20, A21, A19, FUNCT_2:4; verum