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

proof

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

end;

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

proof

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

end;

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