theorem Th40: :: FUNCT_1:41

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