let X, Y be non empty set ; 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; for x being Element of X holds ProjMap1 ((- F),x) = - (ProjMap1 (F,x))
let x be Element of X; ProjMap1 ((- F),x) = - (ProjMap1 (F,x))
now for y being Element of Y holds (ProjMap1 ((- F),x)) . y = (- (ProjMap1 (F,x))) . ylet y be
Element of
Y;
(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;
verum end;
hence
ProjMap1 ((- F),x) = - (ProjMap1 (F,x))
by FUNCT_2:def 8; verum