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

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

let y be Element of Y; :: thesis: (ProjMap1 ((- F),x)) . y = (- (ProjMap1 (F,x))) . y
[x,y] in [:X,Y:] by ZFMISC_1:87;
then A1: [x,y] in dom (- F) by FUNCT_2:def 1;
A2: dom (- (ProjMap1 (F,x))) = Y by FUNCT_2:def 1;
(ProjMap1 ((- F),x)) . y = (- F) . (x,y) by MESFUNC9:def 6;
then (ProjMap1 ((- F),x)) . y = - (F . (x,y)) by A1, MESFUNC1:def 7;
then (ProjMap1 ((- F),x)) . y = - ((ProjMap1 (F,x)) . y) by MESFUNC9:def 6;
hence (ProjMap1 ((- F),x)) . y = (- (ProjMap1 (F,x))) . y by A2, MESFUNC1:def 7; :: thesis: verum

end;

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