set
a
=
curry
f
;
(
dom
f
=
[:
X
,
Y
:]
&
dom
(
curry
f
)
=
proj1
(
dom
f
)
)
by
FUNCT_5:def 1
,
PARTFUN1:def 2
;
then
dom
(
curry
f
)
=
X
by
FUNCT_5:9
;
hence
curry
f
is
X
-defined
by
RELAT_1:def 18
;
:: thesis:
verum