theorem Th32: :: DBLSEQ_3:32

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