let X, Y be set ; :: thesis: for f being Function of X,Y
for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "
let f be Function of X,Y; :: thesis: for g being Function of Y,X st X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one holds
g = f "
let g be Function of Y,X; :: thesis: ( X <> {} & Y <> {} & rng f = Y & g * f = id X & f is one-to-one implies g = f " )
assume ( X <> {} & Y <> {} ) ; :: thesis: ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " )
then ( dom f = X & dom g = Y ) by Def1;
hence ( not rng f = Y or not g * f = id X or not f is one-to-one or g = f " ) by FUNCT_1:41; :: thesis: verum