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 A1: ( f is one-to-one & 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
A2: ( Xa misses Xb & Ya misses Yb & Xa \/ Xb = X & Ya \/ Yb = Y & f .: Xa = Ya & g .: Yb = Xb ) by Th11;
set fXa = f | Xa;
set gYb = g | Yb;
set h = (f | Xa) +* ((g | Yb) " );
dom f = X by FUNCT_2:def 1;
then A3: dom (f | Xa) = Xa by A2, RELAT_1:91, XBOOLE_1:7;
A4: rng (f | Xa) = Ya by A2, RELAT_1:148;
A5: f | Xa is one-to-one by A1, FUNCT_1:84;
dom g = Y by FUNCT_2:def 1;
then A6: dom (g | Yb) = Yb by A2, RELAT_1:91, XBOOLE_1:7;
A7: g | Yb is one-to-one by A1, FUNCT_1:84;
rng (g | Yb) = Xb by A2, RELAT_1:148;
then A8: dom ((g | Yb) " ) = Xb by A7, FUNCT_1:54;
then A9: X = dom ((f | Xa) +* ((g | Yb) " )) by A2, A3, FUNCT_4:def 1;
A10: rng ((g | Yb) " ) = Yb by A6, A7, FUNCT_1:55;
(f | Xa) \/ ((g | Yb) " ) = (f | Xa) +* ((g | Yb) " ) by A2, A3, A8, FUNCT_4:32;
then A11: rng ((f | Xa) +* ((g | Yb) " )) = Y by A2, A4, A10, RELAT_1:26;
then reconsider h = (f | Xa) +* ((g | Yb) " ) as Function of X,Y by A9, FUNCT_2:def 1, RELSET_1:11;
take h ; :: thesis: h is bijective
(g | Yb) " is one-to-one by A7;
then A12: h is one-to-one by A2, A4, A5, A10, FUNCT_4:98;
h is onto by A11, FUNCT_2:def 3;
hence h is bijective by A12, FUNCT_2:def 4; :: thesis: verum