let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL holds max+ f = max- (- f)
let f be PartFunc of X,ExtREAL; :: thesis: max+ f = max- (- f)
- f = (- 1) (#) f by MESFUNC2:9;
then max- (- f) = (- (- 1)) (#) (max+ f) by Th33;
hence max+ f = max- (- f) by MESFUNC2:1; :: thesis: verum