let f, g be Function; :: thesis: ( f is one-to-one & rng g = dom f & f * g = id (rng f) implies g = f " )
assume that
A1: f is one-to-one and
A2: ( rng g = dom f & f * g = id (rng f) ) ; :: thesis: g = f "
( (f ") * f = id (dom f) & dom (f ") = rng f ) by A1, Th32, Th38;
hence g = f " by A2, Lm1; :: thesis: verum