A13
:
dom
g
=
X
by
FUNCT_2:def 1
;
A14
:
dom
(
eq
(
f
,
g
)
)
=
(
dom
f
)
/\
(
dom
g
)
by
Def7
;
A15
:
dom
f
=
X
by
FUNCT_2:def 1
;
rng
(
eq
(
f
,
g
)
)
c=
INT
;
hence
eq
(
f
,
g
) is
Function
of
X
,
INT
by
A14
,
A15
,
A13
,
FUNCT_2:2
;
:: thesis:
verum