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

now :: thesis: for x being Element of X holds (ProjMap2 (F,y)) . x = (ProjMap1 ((~ F),y)) . x

let x be Element of X; :: thesis: (ProjMap2 (F,y)) . x = (ProjMap1 ((~ F),y)) . x
(ProjMap2 (F,y)) . x = F . (x,y) by MESFUNC9:def 7
.= (~ F) . (y,x) by FUNCT_4:def 8 ;
hence (ProjMap2 (F,y)) . x = (ProjMap1 ((~ F),y)) . x by MESFUNC9:def 6; :: thesis: verum

end;

hence ProjMap2 (F,y) = ProjMap1 ((~ F),y) by FUNCT_2:def 8; :: thesis: verum