:: deftheorem Def4 defines ProjPMap2 MESFUN12:def 4 :
for X1, X2 being non empty set
for Y being set
for f being PartFunc of [:X1,X2:],Y
for y being Element of X2
for b₆ being PartFunc of X1,Y holds
( b₆ = ProjPMap2 (f,y) iff ( dom b₆ = Y-section ((dom f),y) & ( for x being Element of X1 st [x,y] in dom f holds
b₆ . x = f . (x,y) ) ) );