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
for
b
_{1}
being
X
-defined
Function
st
b
_{1}
=
curry
f
holds
b
_{1}
is
total
by
PARTFUN1:def 2
;
:: thesis:
verum