for X, Y being 1-sorted
for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds
f " ([#] Y) = [#] X