let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds
( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f )
let f be PartFunc of X,REAL; :: thesis: ( max+ (R_EAL f) = max+ f & max- (R_EAL f) = max- f )
A1: dom (max+ (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 2
.= dom (max+ f) by RFUNCT_3:def 10 ;
now :: thesis: for x being object st x in dom (max+ (R_EAL f)) holds
(max+ (R_EAL f)) . x = (max+ f) . x
let x be object ; :: thesis: ( x in dom (max+ (R_EAL f)) implies (max+ (R_EAL f)) . x = (max+ f) . x )
assume A2: x in dom (max+ (R_EAL f)) ; :: thesis: (max+ (R_EAL f)) . x = (max+ f) . x
then (max+ (R_EAL f)) . x = max+ (f . x) by MESFUNC2:def 2;
hence (max+ (R_EAL f)) . x = (max+ f) . x by A1, A2, RFUNCT_3:def 10; :: thesis: verum
end;
hence max+ (R_EAL f) = max+ f by A1, FUNCT_1:2; :: thesis: max- (R_EAL f) = max- f
A3: dom (max- (R_EAL f)) = dom (R_EAL f) by MESFUNC2:def 3
.= dom (max- f) by RFUNCT_3:def 11 ;
now :: thesis: for x being object st x in dom (max- (R_EAL f)) holds
(max- (R_EAL f)) . x = (max- f) . x
let x be object ; :: thesis: ( x in dom (max- (R_EAL f)) implies (max- (R_EAL f)) . x = (max- f) . x )
assume A4: x in dom (max- (R_EAL f)) ; :: thesis: (max- (R_EAL f)) . x = (max- f) . x
(max- (R_EAL f)) . x = max ((- ((R_EAL f) . x)),0.) by MESFUNC2:def 3, A4;
then (max- (R_EAL f)) . x = max- (f . x) by SUPINF_2:2;
hence (max- (R_EAL f)) . x = (max- f) . x by A3, A4, RFUNCT_3:def 11; :: thesis: verum
end;
hence max- (R_EAL f) = max- f by A3, FUNCT_1:2; :: thesis: verum