theorem Th33: :: FUNCT_1:34

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