for f being Function
for X, x being set st f | X is one-to-one & x in rng (f | X) holds
(f * ((f | X) ")) . x = x