let f be Function; :: thesis: ( f is one-to-one implies ( rng f = dom (f " ) & dom f = rng (f " ) ) )
assume f is one-to-one ; :: thesis: ( rng f = dom (f " ) & dom f = rng (f " ) )
then f " = f ~ by Def9;
hence ( rng f = dom (f " ) & dom f = rng (f " ) ) by RELAT_1:37; :: thesis: verum