theorem Th35: :: FUNCT_1:36

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