let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for A being set holds
( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
let f be PartFunc of X,ExtREAL ; :: thesis: for A being set holds
( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
let A be set ; :: thesis: ( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A )
A1: dom (max+ (f | A)) = dom (f | A) by MESFUNC2:def 2
.= (dom f) /\ A by RELAT_1:90
.= (dom (max+ f)) /\ A by MESFUNC2:def 2
.= dom ((max+ f) | A) by RELAT_1:90 ;
for x being Element of X st x in dom (max+ (f | A)) holds
(max+ (f | A)) . x = ((max+ f) | A) . x

proof

let x be Element of X; :: thesis: ( x in dom (max+ (f | A)) implies (max+ (f | A)) . x = ((max+ f) | A) . x )
assume A2: x in dom (max+ (f | A)) ; :: thesis: (max+ (f | A)) . x = ((max+ f) | A) . x
then x in (dom (max+ f)) /\ A by A1, RELAT_1:90;
then A3: ( x in dom (max+ f) & x in A ) by XBOOLE_0:def 4;
A4: (max+ (f | A)) . x = max ((f | A) . x),0 by A2, MESFUNC2:def 2
.= max (f . x),0 by A3, FUNCT_1:72 ;
((max+ f) | A) . x = (max+ f) . x by A1, A2, FUNCT_1:70;
hence (max+ (f | A)) . x = ((max+ f) | A) . x by A3, A4, MESFUNC2:def 2; :: thesis: verum

end;

hence max+ (f | A) = (max+ f) | A by A1, PARTFUN1:34; :: thesis: max- (f | A) = (max- f) | A
A5: dom (max- (f | A)) = dom (f | A) by MESFUNC2:def 3
.= (dom f) /\ A by RELAT_1:90
.= (dom (max- f)) /\ A by MESFUNC2:def 3
.= dom ((max- f) | A) by RELAT_1:90 ;
for x being Element of X st x in dom (max- (f | A)) holds
(max- (f | A)) . x = ((max- f) | A) . x

proof

let x be Element of X; :: thesis: ( x in dom (max- (f | A)) implies (max- (f | A)) . x = ((max- f) | A) . x )
assume A6: x in dom (max- (f | A)) ; :: thesis: (max- (f | A)) . x = ((max- f) | A) . x
then x in (dom (max- f)) /\ A by A5, RELAT_1:90;
then A7: ( x in dom (max- f) & x in A ) by XBOOLE_0:def 4;
A8: (max- (f | A)) . x = max (- ((f | A) . x)),0 by A6, MESFUNC2:def 3
.= max (- (f . x)),0 by A7, FUNCT_1:72 ;
((max- f) | A) . x = (max- f) . x by A5, A6, FUNCT_1:70;
hence (max- (f | A)) . x = ((max- f) | A) . x by A7, A8, MESFUNC2:def 3; :: thesis: verum

end;

hence max- (f | A) = (max- f) | A by A5, PARTFUN1:34; :: thesis: verum