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