for T, S being 1-sorted
for f being Function of T,S
for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f ") .: P1