let X be non empty set ; :: thesis: for f being PartFunc of X,REAL holds max- f = max+ (- f)
let f be PartFunc of X,REAL; :: thesis: max- f = max+ (- f)
max- f = max- (R_EAL f) by Th30;
then max- f = max+ (- (R_EAL f)) by MESFUNC2:14;
then max- f = max+ (R_EAL (- f)) by Th28;
hence max- f = max+ (- f) by Th30; :: thesis: verum