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