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

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

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

end;

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