theorem :: MESFUN12:30

for X1, X2 being non empty set
for f being PartFunc of [:X1,X2:],ExtREAL
for x being Element of X1
for y being Element of X2 st ( for z being Element of [:X1,X2:] st z in dom f holds
f . z = 0 ) holds
( (ProjPMap2 (f,y)) . x = 0 & (ProjPMap1 (f,x)) . y = 0 )