theorem
Th1
:
:: WAYBEL29:1
for
X
,
Y
being non
empty
set
for
Z
being non
empty
RelStr
for
S
being non
empty
SubRelStr
of
Z
|^
[:
X
,
Y
:]
for
T
being non
empty
SubRelStr
of
(
Z
|^
Y
)
|^
X
for
f
being
Function
of
S
,
T
st
f
is
currying
&
f
is
V7
() &
f
is
onto
holds
f
"
is
uncurrying