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