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 Th55;
then dom (f * (f " )) = dom (f " ) by RELAT_1:46;
hence ( dom (f * (f " )) = rng f & rng (f * (f " )) = rng f ) by A1, A2, Th55, RELAT_1:47; :: thesis: verum