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

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

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

end;

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