theorem Th26: :: MESFUN12:26

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