:: deftheorem defines Proj WAYBEL24:def 2 :
for X1, X2, Y being non empty RelStr
for f being Function of [:X1,X2:],Y
for y being Element of X2 holds Proj (f,y) = (curry' f) . y;