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

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

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

hence
max+ (f | A) = (max+ f) | A
by A1, PARTFUN1:5; :: thesis: max- (f | A) = (max- f) | A
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;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

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

hence
max- (f | A) = (max- f) | A
by A7, PARTFUN1:5; :: thesis: verum
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;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