theorem Th26: :: MESFUNC5:26

for C being non empty set
for f being PartFunc of C,ExtREAL
for c being Real st 0 <= c holds
( max+ (c (#) f) = c (#) (max+ f) & max- (c (#) f) = c (#) (max- f) )