theorem Th46: :: MESFUN12:46

for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for y being Element of X2 holds
( ProjPMap2 ((max+ f),y) = max+ (ProjPMap2 (f,y)) & ProjPMap2 ((max- f),y) = max- (ProjPMap2 (f,y)) )