theorem Th34: :: MESFUN12:34

for X1, X2 being non empty set
for x being Element of X1
for y being Element of X2
for A being Subset of [:X1,X2:]
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) )