let X, Y be non empty set ; :: thesis: for f being Function of X,Y

for g being Function of Y,X st f is one-to-one & g is one-to-one holds

ex h being Function of X,Y st h is bijective

let f be Function of X,Y; :: thesis: for g being Function of Y,X st f is one-to-one & g is one-to-one holds

ex h being Function of X,Y st h is bijective

let g be Function of Y,X; :: thesis: ( f is one-to-one & g is one-to-one implies ex h being Function of X,Y st h is bijective )

assume that

A1: f is one-to-one and

A2: g is one-to-one ; :: thesis: ex h being Function of X,Y st h is bijective

consider Xa, Xb, Ya, Yb being set such that

A3: Xa misses Xb and

A4: Ya misses Yb and

A5: Xa \/ Xb = X and

A6: Ya \/ Yb = Y and

A7: f .: Xa = Ya and

A8: g .: Yb = Xb by Th9;

set gYb = g | Yb;

A9: g | Yb is one-to-one by A2, FUNCT_1:52;

set fXa = f | Xa;

dom f = X by FUNCT_2:def 1;

then A10: dom (f | Xa) = Xa by A5, RELAT_1:62, XBOOLE_1:7;

set h = (f | Xa) +* ((g | Yb) ");

rng (g | Yb) = Xb by A8, RELAT_1:115;

then A11: dom ((g | Yb) ") = Xb by A9, FUNCT_1:32;

then A12: X = dom ((f | Xa) +* ((g | Yb) ")) by A5, A10, FUNCT_4:def 1;

A13: rng (f | Xa) = Ya by A7, RELAT_1:115;

dom g = Y by FUNCT_2:def 1;

then dom (g | Yb) = Yb by A6, RELAT_1:62, XBOOLE_1:7;

then A14: rng ((g | Yb) ") = Yb by A9, FUNCT_1:33;

(f | Xa) \/ ((g | Yb) ") = (f | Xa) +* ((g | Yb) ") by A3, A10, A11, FUNCT_4:31;

then A15: rng ((f | Xa) +* ((g | Yb) ")) = Y by A6, A13, A14, RELAT_1:12;

then reconsider h = (f | Xa) +* ((g | Yb) ") as Function of X,Y by A12, FUNCT_2:def 1, RELSET_1:4;

A16: h is onto by A15, FUNCT_2:def 3;

take h ; :: thesis: h is bijective

f | Xa is one-to-one by A1, FUNCT_1:52;

then h is one-to-one by A4, A13, A9, A14, FUNCT_4:92;

hence h is bijective by A16, FUNCT_2:def 4; :: thesis: verum

for g being Function of Y,X st f is one-to-one & g is one-to-one holds

ex h being Function of X,Y st h is bijective

let f be Function of X,Y; :: thesis: for g being Function of Y,X st f is one-to-one & g is one-to-one holds

ex h being Function of X,Y st h is bijective

let g be Function of Y,X; :: thesis: ( f is one-to-one & g is one-to-one implies ex h being Function of X,Y st h is bijective )

assume that

A1: f is one-to-one and

A2: g is one-to-one ; :: thesis: ex h being Function of X,Y st h is bijective

consider Xa, Xb, Ya, Yb being set such that

A3: Xa misses Xb and

A4: Ya misses Yb and

A5: Xa \/ Xb = X and

A6: Ya \/ Yb = Y and

A7: f .: Xa = Ya and

A8: g .: Yb = Xb by Th9;

set gYb = g | Yb;

A9: g | Yb is one-to-one by A2, FUNCT_1:52;

set fXa = f | Xa;

dom f = X by FUNCT_2:def 1;

then A10: dom (f | Xa) = Xa by A5, RELAT_1:62, XBOOLE_1:7;

set h = (f | Xa) +* ((g | Yb) ");

rng (g | Yb) = Xb by A8, RELAT_1:115;

then A11: dom ((g | Yb) ") = Xb by A9, FUNCT_1:32;

then A12: X = dom ((f | Xa) +* ((g | Yb) ")) by A5, A10, FUNCT_4:def 1;

A13: rng (f | Xa) = Ya by A7, RELAT_1:115;

dom g = Y by FUNCT_2:def 1;

then dom (g | Yb) = Yb by A6, RELAT_1:62, XBOOLE_1:7;

then A14: rng ((g | Yb) ") = Yb by A9, FUNCT_1:33;

(f | Xa) \/ ((g | Yb) ") = (f | Xa) +* ((g | Yb) ") by A3, A10, A11, FUNCT_4:31;

then A15: rng ((f | Xa) +* ((g | Yb) ")) = Y by A6, A13, A14, RELAT_1:12;

then reconsider h = (f | Xa) +* ((g | Yb) ") as Function of X,Y by A12, FUNCT_2:def 1, RELSET_1:4;

A16: h is onto by A15, FUNCT_2:def 3;

take h ; :: thesis: h is bijective

f | Xa is one-to-one by A1, FUNCT_1:52;

then h is one-to-one by A4, A13, A9, A14, FUNCT_4:92;

hence h is bijective by A16, FUNCT_2:def 4; :: thesis: verum