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 f " is currying by Th3;
then ( f is monotone & f " is monotone & f * (f " ) = id T & (f " ) * f = id S ) by A1, GRCAT_1:56, WAYBEL27:20, WAYBEL27:21;
hence f is isomorphic by YELLOW16:17; :: thesis: verum