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