let X, Y be 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
let Z be 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
let T be 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
let S be 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
let f be Function of S,T; ( f is uncurrying & f is V7() & f is onto implies f is isomorphic )
assume A1:
( f is uncurrying & f is V7() & f is onto )
; f is isomorphic
then A2:
( f * (f ") = id T & (f ") * f = id S )
by GRCAT_1:41;
( f is monotone & f " is monotone )
by A1, Th2, WAYBEL27:20, WAYBEL27:21;
hence
f is isomorphic
by A2, YELLOW16:15; verum