theorem Th35: :: GROUP_21:2

for X, Y being non empty set
for X0, Y0 being set
for f being Function of X,Y st f is bijective & rng (f | X0) = Y0 holds
(f | X0) " = (f ") | Y0