for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2
for x being Element of X1 holds (Proj (f,y)) . x = f . (x,y)