theorem Th35: :: MESFUN12:35

for X1, X2 being non empty set
for A being Subset of [:X1,X2:]
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )