for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T
for X being Subset of T holds (f " X) ` = f " (X `)