let X1, X2 be non empty set ; :: thesis: for E being Subset of [:X1,X2:]
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )
let E be Subset of [:X1,X2:]; :: thesis: for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )
let x be Element of X1; :: thesis: for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )
let y be Element of X2; :: thesis: ( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) )
for y being Element of X2 holds (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y

proof

let y be Element of X2; :: thesis: (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y
A1: (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi (E,[:X1,X2:])) . (x,y) by MESFUNC9:def 6;
then A2: ( [x,y] in E implies (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = 1 ) by FUNCT_3:def 3;
[x,y] is Element of [:X1,X2:] by ZFMISC_1:def 2;
then A3: ( not [x,y] in E implies (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = 0 ) by A1, FUNCT_3:def 3;

per cases ( [x,y] in E or not [x,y] in E ) ;

suppose A4: [x,y] in E ; :: thesis: (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y

then y in X-section (E,x) by Th25;
hence (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y by A2, A4, FUNCT_3:def 3; :: thesis: verum

end;

suppose A5: not [x,y] in E ; :: thesis: (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y

then not y in X-section (E,x) by Th25;
hence (ProjMap1 ((chi (E,[:X1,X2:])),x)) . y = (chi ((X-section (E,x)),X2)) . y by A3, A5, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

then ProjMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) by FUNCT_2:def 8;
hence ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((X-section (E,x)),X2) by Th27; :: thesis: ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1)
for x being Element of X1 holds (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x

proof

let x be Element of X1; :: thesis: (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x
A1: (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi (E,[:X1,X2:])) . (x,y) by MESFUNC9:def 7;
then A2: ( [x,y] in E implies (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = 1 ) by FUNCT_3:def 3;
[x,y] is Element of [:X1,X2:] by ZFMISC_1:def 2;
then A3: ( not [x,y] in E implies (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = 0 ) by A1, FUNCT_3:def 3;

per cases ( [x,y] in E or not [x,y] in E ) ;

suppose A4: [x,y] in E ; :: thesis: (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x

then x in Y-section (E,y) by Th25;
hence (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x by A2, A4, FUNCT_3:def 3; :: thesis: verum

end;

suppose A5: not [x,y] in E ; :: thesis: (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x

then not x in Y-section (E,y) by Th25;
hence (ProjMap2 ((chi (E,[:X1,X2:])),y)) . x = (chi ((Y-section (E,y)),X1)) . x by A3, A5, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

then ProjMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) by FUNCT_2:def 8;
hence ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Y-section (E,y)),X1) by Th27; :: thesis: verum