theorem Th34: :: FUNCT_1:35

for y being object
for f being Function st f is one-to-one & y in rng f holds
( y = f . ((f ") . y) & y = (f * (f ")) . y )