let f be Function; :: thesis: ( f is one-to-one implies ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f ) )
assume A1: f is one-to-one ; :: thesis: ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f )
then A2: rng (f ") = dom f by Th32;
then dom (f * (f ")) = dom (f ") by RELAT_1:27;
hence ( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f ) by A1, A2, Th32, RELAT_1:28; :: thesis: verum