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