theorem Th38: :: FUNCT_1:39

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