let C be non empty set ; :: thesis: for f being PartFunc of C,ExtREAL holds max- f = max+ (- f)
let f be PartFunc of C,ExtREAL; :: thesis: max- f = max+ (- f)
A1: dom (max- f) = dom f by Def3
.= dom (- f) by MESFUNC1:def 7 ;
then A2: dom (max- f) = dom (max+ (- f)) by Def2;
for x being Element of C st x in dom (max- f) holds
(max- f) . x = (max+ (- f)) . x

proof

let x be Element of C; :: thesis: ( x in dom (max- f) implies (max- f) . x = (max+ (- f)) . x )
assume A3: x in dom (max- f) ; :: thesis: (max- f) . x = (max+ (- f)) . x
then ( (max- f) . x = max ((- (f . x)),0.) & - (f . x) = (- f) . x ) by A1, Def3, MESFUNC1:def 7;
hence (max- f) . x = (max+ (- f)) . x by A2, A3, Def2; :: thesis: verum

end;

hence max- f = max+ (- f) by A2, PARTFUN1:5; :: thesis: verum