let X1, X2 be non empty set ; :: thesis: 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)) )
let x be Element of X1; :: thesis: 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)) )
let y be Element of X2; :: thesis: 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)) )
let A be Subset of [:X1,X2:]; :: thesis: 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)) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) )
set f1 = f | A;
A2: (dom f) /\ A c= dom f by XBOOLE_1:17;
A4: dom (f | A) = (dom f) /\ A by RELAT_1:61;
A7: dom ((ProjPMap1 (f,x)) | (X-section (A,x))) = (dom (ProjPMap1 (f,x))) /\ (X-section (A,x)) by RELAT_1:61
.= (X-section ((dom f),x)) /\ (X-section (A,x)) by Def3
.= X-section (((dom f) /\ A),x) by MEASUR11:27
.= dom (ProjPMap1 ((f | A),x)) by A4, Def3 ;

now :: thesis: for y being Element of X2 st y in dom (ProjPMap1 ((f | A),x)) holds
(ProjPMap1 ((f | A),x)) . y = ((ProjPMap1 (f,x)) | (X-section (A,x))) . y

let y be Element of X2; :: thesis: ( y in dom (ProjPMap1 ((f | A),x)) implies (ProjPMap1 ((f | A),x)) . y = ((ProjPMap1 (f,x)) | (X-section (A,x))) . y )
assume y in dom (ProjPMap1 ((f | A),x)) ; :: thesis: (ProjPMap1 ((f | A),x)) . y = ((ProjPMap1 (f,x)) | (X-section (A,x))) . y
then A8: y in X-section (((dom f) /\ A),x) by A4, Def3;
then A9: [x,y] in (dom f) /\ A by Th25;
then (ProjPMap1 ((f | A),x)) . y = (f | A) . (x,y) by A4, Def3;
then A10: (ProjPMap1 ((f | A),x)) . y = f . (x,y) by A9, FUNCT_1:48;
b3: (ProjPMap1 (f,x)) . y = f . (x,y) by A2, A9, Def3;
y in (X-section ((dom f),x)) /\ (X-section (A,x)) by A8, MEASUR11:27;
then y in X-section (A,x) by XBOOLE_0:def 4;
hence (ProjPMap1 ((f | A),x)) . y = ((ProjPMap1 (f,x)) | (X-section (A,x))) . y by A10, b3, FUNCT_1:49; :: thesis: verum

end;

hence ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) by A7, PARTFUN1:5; :: thesis: ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y))
A13: dom ((ProjPMap2 (f,y)) | (Y-section (A,y))) = (dom (ProjPMap2 (f,y))) /\ (Y-section (A,y)) by RELAT_1:61
.= (Y-section ((dom f),y)) /\ (Y-section (A,y)) by Def4
.= Y-section (((dom f) /\ A),y) by MEASUR11:27
.= dom (ProjPMap2 ((f | A),y)) by A4, Def4 ;

now :: thesis: for x being Element of X1 st x in dom (ProjPMap2 ((f | A),y)) holds
(ProjPMap2 ((f | A),y)) . x = ((ProjPMap2 (f,y)) | (Y-section (A,y))) . x

let x be Element of X1; :: thesis: ( x in dom (ProjPMap2 ((f | A),y)) implies (ProjPMap2 ((f | A),y)) . x = ((ProjPMap2 (f,y)) | (Y-section (A,y))) . x )
assume x in dom (ProjPMap2 ((f | A),y)) ; :: thesis: (ProjPMap2 ((f | A),y)) . x = ((ProjPMap2 (f,y)) | (Y-section (A,y))) . x
then A14: x in Y-section (((dom f) /\ A),y) by A4, Def4;
then A15: [x,y] in (dom f) /\ A by Th25;
then (ProjPMap2 ((f | A),y)) . x = (f | A) . (x,y) by A4, Def4;
then A16: (ProjPMap2 ((f | A),y)) . x = f . (x,y) by A15, FUNCT_1:48;
b4: (ProjPMap2 (f,y)) . x = f . (x,y) by A2, A15, Def4;
x in (Y-section ((dom f),y)) /\ (Y-section (A,y)) by A14, MEASUR11:27;
then x in Y-section (A,y) by XBOOLE_0:def 4;
hence (ProjPMap2 ((f | A),y)) . x = ((ProjPMap2 (f,y)) | (Y-section (A,y))) . x by A16, b4, FUNCT_1:49; :: thesis: verum

end;

hence ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) by A13, PARTFUN1:5; :: thesis: verum