theorem :: WAYBEL29:4

for X, Y being non empty set
for Z being non empty Poset
for T being non empty full SubRelStr of Z |^ [:X,Y:]
for S being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is uncurrying & f is V7() & f is onto holds
f is isomorphic