let f be Function; :: thesis: ( f is one-to-one implies (f ") " = f )
assume A1: f is one-to-one ; :: thesis: (f ") " = f
then rng f = dom (f ") by Th55;
then A2: f * (f ") = id (dom (f ")) by A1, Th61;
dom f = rng (f ") by A1, Th55;
hence (f ") " = f by A1, A2, Th63; :: thesis: verum