theorem
Th2
:
:: WAYBEL29:2
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
T
,
S
st
f
is
uncurrying
&
f
is
V7
() &
f
is
onto
holds
f
"
is
currying