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