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:61
.= (dom (max+ f)) /\ A by MESFUNC2:def 2
.= dom ((max+ f) | A) by RELAT_1:61 ;
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 A3: ((max+ f) | A) . x = (max+ f) . x by A1, FUNCT_1:47;
A4: x in (dom (max+ f)) /\ A by A1, A2, RELAT_1:61;
then A5: x in dom (max+ f) by XBOOLE_0:def 4;
A6: x in A by A4, XBOOLE_0:def 4;
(max+ (f | A)) . x = max (((f | A) . x),0) by A2, MESFUNC2:def 2
.= max ((f . x),0) by A6, FUNCT_1:49 ;
hence (max+ (f | A)) . x = ((max+ f) | A) . x by A5, A3, MESFUNC2:def 2; :: thesis: verum

end;

hence max+ (f | A) = (max+ f) | A by A1, PARTFUN1:5; :: thesis: max- (f | A) = (max- f) | A
A7: dom (max- (f | A)) = dom (f | A) by MESFUNC2:def 3
.= (dom f) /\ A by RELAT_1:61
.= (dom (max- f)) /\ A by MESFUNC2:def 3
.= dom ((max- f) | A) by RELAT_1:61 ;
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 A8: x in dom (max- (f | A)) ; :: thesis: (max- (f | A)) . x = ((max- f) | A) . x
then A9: ((max- f) | A) . x = (max- f) . x by A7, FUNCT_1:47;
A10: x in (dom (max- f)) /\ A by A7, A8, RELAT_1:61;
then A11: x in dom (max- f) by XBOOLE_0:def 4;
A12: x in A by A10, XBOOLE_0:def 4;
(max- (f | A)) . x = max ((- ((f | A) . x)),0) by A8, MESFUNC2:def 3
.= max ((- (f . x)),0) by A12, FUNCT_1:49 ;
hence (max- (f | A)) . x = ((max- f) | A) . x by A11, A9, MESFUNC2:def 3; :: thesis: verum

end;

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