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

end;

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