theorem Th42: :: MESFUN12:42

for X1, X2 being non empty set
for A, Z being set
for f being PartFunc of [:X1,X2:],Z
for y being Element of X2 holds Y-section ((f " A),y) = (ProjPMap2 (f,y)) " A