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 Th32;
then A2: f * (f ") = id (dom (f ")) by A1, Th38;
dom f = rng (f ") by A1, Th32;
hence (f ") " = f by A1, A2, Th40; :: thesis: verum