let X be non empty set ; :: thesis: for Y being set
for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
let Y be set ; :: thesis: for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
let f be PartFunc of X,REAL; :: thesis: ( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )
A1: dom (max+ (f | Y)) = dom (f | Y) by RFUNCT_3:def 10
.= (dom f) /\ Y by RELAT_1:61
.= (dom (max+ f)) /\ Y by RFUNCT_3:def 10
.= dom ((max+ f) | Y) by RELAT_1:61 ;
for x being Element of X st x in dom (max+ (f | Y)) holds
(max+ (f | Y)) . x = ((max+ f) | Y) . x

proof

let x be Element of X; :: thesis: ( x in dom (max+ (f | Y)) implies (max+ (f | Y)) . x = ((max+ f) | Y) . x )
assume A2: x in dom (max+ (f | Y)) ; :: thesis: (max+ (f | Y)) . x = ((max+ f) | Y) . x
then A3: x in (dom (max+ f)) /\ Y by A1, RELAT_1:61;
then A4: x in Y by XBOOLE_0:def 4;
A5: x in dom (max+ f) by A3, XBOOLE_0:def 4;
A6: (max+ (f | Y)) . x = max+ ((f | Y) . x) by A2, RFUNCT_3:def 10
.= max ((f . x),0) by A4, FUNCT_1:49 ;
((max+ f) | Y) . x = (max+ f) . x by A1, A2, FUNCT_1:47
.= max+ (f . x) by A5, RFUNCT_3:def 10 ;
hence (max+ (f | Y)) . x = ((max+ f) | Y) . x by A6; :: thesis: verum

end;

hence max+ (f | Y) = (max+ f) | Y by A1, PARTFUN1:5; :: thesis: max- (f | Y) = (max- f) | Y
A7: dom (max- (f | Y)) = dom (f | Y) by RFUNCT_3:def 11
.= (dom f) /\ Y by RELAT_1:61
.= (dom (max- f)) /\ Y by RFUNCT_3:def 11
.= dom ((max- f) | Y) by RELAT_1:61 ;
for x being Element of X st x in dom (max- (f | Y)) holds
(max- (f | Y)) . x = ((max- f) | Y) . x

proof

let x be Element of X; :: thesis: ( x in dom (max- (f | Y)) implies (max- (f | Y)) . x = ((max- f) | Y) . x )
assume A8: x in dom (max- (f | Y)) ; :: thesis: (max- (f | Y)) . x = ((max- f) | Y) . x
then A9: x in (dom (max- f)) /\ Y by A7, RELAT_1:61;
then A10: x in Y by XBOOLE_0:def 4;
A11: x in dom (max- f) by A9, XBOOLE_0:def 4;
A12: (max- (f | Y)) . x = max- ((f | Y) . x) by A8, RFUNCT_3:def 11
.= max ((- (f . x)),0) by A10, FUNCT_1:49 ;
((max- f) | Y) . x = (max- f) . x by A7, A8, FUNCT_1:47
.= max- (f . x) by A11, RFUNCT_3:def 11 ;
hence (max- (f | Y)) . x = ((max- f) | Y) . x by A12; :: thesis: verum

end;

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