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 one-to-one & f is onto holds
f " is uncurrying