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