theorem Th41: :: MESFUN12:41

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