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 and
A3: g * f = id (dom f) ; :: thesis: g = f "
( f * (f " ) = id (rng f) & rng (f " ) = dom f ) by A1, Th55, Th61;
hence g = f " by A2, A3, Lm1; :: thesis: verum