let X1, X2 be 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)) )
let x be 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 y be 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 A be 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 f be PartFunc of [:X1,X2:],ExtREAL; ( 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 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))) . ylet y be
Element of
X2;
( 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))
;
(ProjPMap1 ((f | A),x)) . y = ((ProjPMap1 (f,x)) | (X-section (A,x))) . ythen 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;
verum end;
hence
ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x))
by A7, PARTFUN1:5; 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 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))) . xlet x be
Element of
X1;
( 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))
;
(ProjPMap2 ((f | A),y)) . x = ((ProjPMap2 (f,y)) | (Y-section (A,y))) . xthen 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;
verum end;
hence
ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y))
by A13, PARTFUN1:5; verum