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:90
.= (dom (max+ f)) /\ Y by RFUNCT_3:def 10
.= dom ((max+ f) | Y) by RELAT_1:90 ;
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 x in (dom (max+ f)) /\ Y by A1, RELAT_1:90;
then A3: ( x in dom (max+ f) & x in Y ) by XBOOLE_0:def 4;
A4: (max+ (f | Y)) . x = max+ ((f | Y) . x) by A2, RFUNCT_3:def 10
.= max (f . x),0 by A3, FUNCT_1:72 ;
((max+ f) | Y) . x = (max+ f) . x by A1, A2, FUNCT_1:70
.= max+ (f . x) by A3, RFUNCT_3:def 10 ;
hence (max+ (f | Y)) . x = ((max+ f) | Y) . x by A4; :: thesis: verum

end;

hence max+ (f | Y) = (max+ f) | Y by A1, PARTFUN1:34; :: thesis: max- (f | Y) = (max- f) | Y
A5: dom (max- (f | Y)) = dom (f | Y) by RFUNCT_3:def 11
.= (dom f) /\ Y by RELAT_1:90
.= (dom (max- f)) /\ Y by RFUNCT_3:def 11
.= dom ((max- f) | Y) by RELAT_1:90 ;
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 A6: x in dom (max- (f | Y)) ; :: thesis: (max- (f | Y)) . x = ((max- f) | Y) . x
then x in (dom (max- f)) /\ Y by A5, RELAT_1:90;
then A7: ( x in dom (max- f) & x in Y ) by XBOOLE_0:def 4;
A8: (max- (f | Y)) . x = max- ((f | Y) . x) by A6, RFUNCT_3:def 11
.= max (- (f . x)),0 by A7, FUNCT_1:72 ;
((max- f) | Y) . x = (max- f) . x by A5, A6, FUNCT_1:70
.= max- (f . x) by A7, RFUNCT_3:def 11 ;
hence (max- (f | Y)) . x = ((max- f) | Y) . x by A8; :: thesis: verum

end;

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