for X, Y, Z being set
for f being Function of X,Y st ( Y = {} implies X = {} ) & Z c= X holds
f | Z is Function of Z,Y