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 V7() & 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 V7() & 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 V7() & 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 V7() & f is onto holds

f is isomorphic

let f be Function of S,T; :: thesis: ( f is uncurrying & f is V7() & f is onto implies f is isomorphic )

assume A1: ( f is uncurrying & 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 A1, Th2, WAYBEL27:20, WAYBEL27:21;

hence f is isomorphic by A2, YELLOW16:15; :: thesis: verum

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; :: 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 V7() & 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 V7() & 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 V7() & f is onto holds

f is isomorphic

let f be Function of S,T; :: thesis: ( f is uncurrying & f is V7() & f is onto implies f is isomorphic )

assume A1: ( f is uncurrying & 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 A1, Th2, WAYBEL27:20, WAYBEL27:21;

hence f is isomorphic by A2, YELLOW16:15; :: thesis: verum