for f being Function st f is one-to-one holds
( dom (f * (f ")) = rng f & rng (f * (f ")) = rng f )