theorem :: MESFUNC6:66

for X being non empty set
for Y being set
for f being PartFunc of X,REAL holds
( max+ (f | Y) = (max+ f) | Y & max- (f | Y) = (max- f) | Y )