for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f ") = [#] S & rng (f ") = [#] T )