let X, Y be non empty set ; :: thesis: 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 one-to-one & f is onto holds
f is isomorphic
let Z be non empty Poset; :: thesis: 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 one-to-one & f is onto holds
f is isomorphic
let T be non empty full SubRelStr of Z |^ [:X,Y:]; :: thesis: for S being non empty full SubRelStr of (Z |^ Y) |^ X
for f being Function of S,T st f is uncurrying & f is one-to-one & f is onto holds
f is isomorphic
let S be non empty full SubRelStr of (Z |^ Y) |^ X; :: thesis: for f being Function of S,T st f is uncurrying & f is one-to-one & f is onto holds
f is isomorphic
let f be Function of S,T; :: thesis: ( f is uncurrying & f is one-to-one & f is onto implies f is isomorphic )
assume A1: ( f is uncurrying & f is one-to-one & 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 A1, Th2, WAYBEL27:20, WAYBEL27:21;
hence f is isomorphic by A2, YELLOW16:15; :: thesis: verum