theorem :: FUNCT_2:26

for X, Y being set
for x being object
for f being Function of X,Y st Y <> {} & f is one-to-one & x in X holds
(f ") . (f . x) = x