theorem Th32: :: MESFUN12:32
for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds
( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )