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 Def5;
hence ( rng f = dom (f ") & dom f = rng (f ") ) by RELAT_1:20; :: thesis: verum