theorem Th33: :: DBLSEQ_3:33

for X, Y, Z being non empty set
for F being Function of [:X,Y:],Z
for y being Element of Y holds ProjMap2 (F,y) = ProjMap1 ((~ F),y)