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 A4: (max- f) . x = max (- (f . x)),0. by Def3;
- (f . x) = (- f) . x by A1, A3, MESFUNC1:def 7;
hence (max- f) . x = (max+ (- f)) . x by A2, A3, A4, Def2; :: thesis: verum

end;

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