theorem Th9: :: WAYBEL24:9

for R, S, T being non empty RelStr
for f being Function of [:R,S:],T
for a being Element of R
for b being Element of S holds (Proj (f,a)) . b = (Proj (f,b)) . a