let X, Y be non empty set ; :: thesis: for Z being non empty Poset
for S being non empty full SubRelStr of Z |^ [:X,Y:]
for T being non empty full 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 isomorphic

let Z be non empty Poset; :: thesis: for S being non empty full SubRelStr of Z |^ [:X,Y:]
for T being non empty full 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 isomorphic

let S be non empty full SubRelStr of Z |^ [:X,Y:]; :: thesis: for T being non empty full 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 isomorphic

let T be non empty full SubRelStr of (Z |^ Y) |^ X; :: thesis: for f being Function of S,T st f is currying & f is V7() & f is onto holds
f is isomorphic

let f be Function of S,T; :: thesis: ( f is currying & f is V7() & f is onto implies f is isomorphic )
assume A1: ( f is currying & f is V7() & f is onto ) ; :: thesis: f is isomorphic
then A2: ( f * (f ") = id T & (f ") * f = id S ) by GRCAT_1:41;
( f is monotone & f " is monotone ) by ;
hence f is isomorphic by ; :: thesis: verum