let X1, X2 be non empty set ; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1 holds
( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: for x being Element of X1 holds
( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )
let x be Element of X1; :: thesis: ( ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) & ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) )
( dom (ProjPMap1 ((max+ f),x)) = X-section ((dom (max+ f)),x) & dom (ProjPMap1 ((max- f),x)) = X-section ((dom (max- f)),x) ) by Def3;
then A1: ( dom (ProjPMap1 ((max+ f),x)) = X-section ((dom f),x) & dom (ProjPMap1 ((max- f),x)) = X-section ((dom f),x) ) by MESFUNC2:def 2, MESFUNC2:def 3;
( dom (max+ (ProjPMap1 (f,x))) = dom (ProjPMap1 (f,x)) & dom (max- (ProjPMap1 (f,x))) = dom (ProjPMap1 (f,x)) ) by MESFUNC2:def 2, MESFUNC2:def 3;
then A2: ( dom (max+ (ProjPMap1 (f,x))) = X-section ((dom f),x) & dom (max- (ProjPMap1 (f,x))) = X-section ((dom f),x) ) by Def3;
for y being Element of X2 st y in dom (ProjPMap1 ((max+ f),x)) holds
(ProjPMap1 ((max+ f),x)) . y = (max+ (ProjPMap1 (f,x))) . y

proof

let y be Element of X2; :: thesis: ( y in dom (ProjPMap1 ((max+ f),x)) implies (ProjPMap1 ((max+ f),x)) . y = (max+ (ProjPMap1 (f,x))) . y )
assume A3: y in dom (ProjPMap1 ((max+ f),x)) ; :: thesis: (ProjPMap1 ((max+ f),x)) . y = (max+ (ProjPMap1 (f,x))) . y
then y in { y where y is Element of X2 : [x,y] in dom f } by A1, MEASUR11:def 4;
then A4: ex y1 being Element of X2 st
( y1 = y & [x,y1] in dom f ) ;
set z = [x,y];
A5: [x,y] in dom (max+ f) by A4, MESFUNC2:def 2;
then A6: (ProjPMap1 ((max+ f),x)) . y = (max+ f) . (x,y) by Def3
.= max ((f . [x,y]),0) by A5, MESFUNC2:def 2 ;
(ProjPMap1 (f,x)) . y = f . (x,y) by A4, Def3;
hence (ProjPMap1 ((max+ f),x)) . y = (max+ (ProjPMap1 (f,x))) . y by A6, A1, A3, A2, MESFUNC2:def 2; :: thesis: verum

end;

hence ProjPMap1 ((max+ f),x) = max+ (ProjPMap1 (f,x)) by A1, A2, PARTFUN1:5; :: thesis: ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x))
for y being Element of X2 st y in dom (ProjPMap1 ((max- f),x)) holds
(ProjPMap1 ((max- f),x)) . y = (max- (ProjPMap1 (f,x))) . y

proof

let y be Element of X2; :: thesis: ( y in dom (ProjPMap1 ((max- f),x)) implies (ProjPMap1 ((max- f),x)) . y = (max- (ProjPMap1 (f,x))) . y )
assume A8: y in dom (ProjPMap1 ((max- f),x)) ; :: thesis: (ProjPMap1 ((max- f),x)) . y = (max- (ProjPMap1 (f,x))) . y
then y in { y where y is Element of X2 : [x,y] in dom f } by A1, MEASUR11:def 4;
then A9: ex y1 being Element of X2 st
( y1 = y & [x,y1] in dom f ) ;
set z = [x,y];
A10: [x,y] in dom (max- f) by A9, MESFUNC2:def 3;
then A11: (ProjPMap1 ((max- f),x)) . y = (max- f) . (x,y) by Def3
.= max ((- (f . [x,y])),0) by A10, MESFUNC2:def 3 ;
(ProjPMap1 (f,x)) . y = f . (x,y) by A9, Def3;
hence (ProjPMap1 ((max- f),x)) . y = (max- (ProjPMap1 (f,x))) . y by A11, A1, A2, A8, MESFUNC2:def 3; :: thesis: verum

end;

hence ProjPMap1 ((max- f),x) = max- (ProjPMap1 (f,x)) by A1, A2, PARTFUN1:5; :: thesis: verum