:: deftheorem Def3 defines ProjPMap1 MESFUN12:def 3 :
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 b₆ being PartFunc of X2,Y holds
( b₆ = ProjPMap1 (f,x) iff ( dom b₆ = X-section ((dom f),x) & ( for y being Element of X2 st [x,y] in dom f holds
b₆ . y = f . (x,y) ) ) );