theorem :: MESFUNC6:63
for X being non empty set
for f, g being PartFunc of X,REAL holds ((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)