theorem Th25: :: MESFUNC5:25

for X being non empty set
for f, g being PartFunc of X,ExtREAL st f is () & f is () & g is () & g is () holds
((max+ (f + g)) + (max- f)) + (max- g) = ((max- (f + g)) + (max+ f)) + (max+ g)