let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds
( max+ () = R_EAL (max+ f) & max- () = R_EAL (max- f) )

let f be PartFunc of X,REAL; :: thesis: ( max+ () = R_EAL (max+ f) & max- () = R_EAL (max- f) )
dom (max+ ()) = dom () by MESFUNC2:def 2;
then dom (max+ ()) = dom f by MESFUNC5:def 7;
then A1: dom (max+ ()) = dom (max+ f) by RFUNCT_3:def 10;
then A2: dom (max+ ()) = dom (R_EAL (max+ f)) by MESFUNC5:def 7;
dom (max- ()) = dom () by MESFUNC2:def 3;
then dom (max- ()) = dom f by MESFUNC5:def 7;
then A3: dom (max- ()) = dom (max- f) by RFUNCT_3:def 11;
then A4: dom (max- ()) = dom (R_EAL (max- f)) by MESFUNC5:def 7;
for x being Element of X st x in dom (max+ ()) holds
(max+ ()) . x = (R_EAL (max+ f)) . x
proof
let x be Element of X; :: thesis: ( x in dom (max+ ()) implies (max+ ()) . x = (R_EAL (max+ f)) . x )
assume A5: x in dom (max+ ()) ; :: thesis: (max+ ()) . x = (R_EAL (max+ f)) . x
per cases ( f . x >= 0 or f . x < 0 ) ;
suppose A6: f . x >= 0 ; :: thesis: (max+ ()) . x = (R_EAL (max+ f)) . x
then A7: (R_EAL f) . x >= 0 by MESFUNC5:def 7;
(max+ ()) . x = max ((() . x),0) by ;
then (max+ ()) . x = () . x by ;
then (max+ ()) . x = f . x by MESFUNC5:def 7;
then (max+ ()) . x = max ((f . x),0) by ;
then (max+ ()) . x = max+ (f . x) by RFUNCT_3:def 1;
then (max+ ()) . x = (max+ f) . x by ;
hence (max+ ()) . x = (R_EAL (max+ f)) . x by MESFUNC5:def 7; :: thesis: verum
end;
suppose A8: f . x < 0 ; :: thesis: (max+ ()) . x = (R_EAL (max+ f)) . x
then A9: (R_EAL f) . x < 0 by MESFUNC5:def 7;
(max+ ()) . x = max ((() . x),0) by ;
then (max+ ()) . x = 0 by ;
then (max+ ()) . x = max ((f . x),0) by ;
then (max+ ()) . x = max+ (f . x) by RFUNCT_3:def 1;
then (max+ ()) . x = (max+ f) . x by ;
hence (max+ ()) . x = (R_EAL (max+ f)) . x by MESFUNC5:def 7; :: thesis: verum
end;
end;
end;
hence max+ () = R_EAL (max+ f) by ; :: thesis: max- () = R_EAL (max- f)
for x being Element of X st x in dom (max- ()) holds
(max- ()) . x = (R_EAL (max- f)) . x
proof
let x be Element of X; :: thesis: ( x in dom (max- ()) implies (max- ()) . x = (R_EAL (max- f)) . x )
assume A10: x in dom (max- ()) ; :: thesis: (max- ()) . x = (R_EAL (max- f)) . x
per cases ( f . x <= 0 or f . x > 0 ) ;
suppose A11: f . x <= 0 ; :: thesis: (max- ()) . x = (R_EAL (max- f)) . x
then A12: (R_EAL f) . x <= 0 by MESFUNC5:def 7;
(max- ()) . x = max ((- (() . x)),0) by ;
then (max- ()) . x = - (() . x) by ;
then (max- ()) . x = - (f . x) by MESFUNC5:def 7;
then (max- ()) . x = max ((- (f . x)),0) by ;
then (max- ()) . x = max- (f . x) by RFUNCT_3:def 2;
then (max- ()) . x = (max- f) . x by ;
hence (max- ()) . x = (R_EAL (max- f)) . x by MESFUNC5:def 7; :: thesis: verum
end;
suppose A13: f . x > 0 ; :: thesis: (max- ()) . x = (R_EAL (max- f)) . x
then A14: (R_EAL f) . x > 0 by MESFUNC5:def 7;
(max- ()) . x = max ((- (() . x)),0) by ;
then (max- ()) . x = 0 by ;
then (max- ()) . x = max ((- (f . x)),0) by ;
then (max- ()) . x = max- (f . x) by RFUNCT_3:def 2;
then (max- ()) . x = (max- f) . x by ;
hence (max- ()) . x = (R_EAL (max- f)) . x by MESFUNC5:def 7; :: thesis: verum
end;
end;
end;
hence max- () = R_EAL (max- f) by ; :: thesis: verum