let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )
let S2 be SigmaField of X2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (E,[:X1,X2:])),x) = chi ((Measurable-X-section (E,x)),X2) & ProjPMap2 ((chi (E,[:X1,X2:])),y) = chi ((Measurable-Y-section (E,y)),X1) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((chi (A,[:X1,X2:])),x) = chi ((Measurable-X-section (A,x)),X2) & ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1) )
let x be Element of X1; :: thesis: for y being Element of X2 holds
( ProjPMap1 ((chi (A,[:X1,X2:])),x) = chi ((Measurable-X-section (A,x)),X2) & ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1) )
let y be Element of X2; :: thesis: ( ProjPMap1 ((chi (A,[:X1,X2:])),x) = chi ((Measurable-X-section (A,x)),X2) & ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1) )
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
A1: ( x in XX1 implies X-section ([:XX1,XX2:],x) = XX2 ) by MEASUR11:22;
dom (ProjPMap1 ((chi (A,[:X1,X2:])),x)) = X-section ((dom (chi (A,[:X1,X2:]))),x) by Def3
.= X-section (XX12,x) by FUNCT_3:def 3 ;
then A2: dom (ProjPMap1 ((chi (A,[:X1,X2:])),x)) = dom (chi ((Measurable-X-section (A,x)),X2)) by A1, FUNCT_3:def 3;

now :: thesis: for y being Element of X2 st y in dom (ProjPMap1 ((chi (A,[:X1,X2:])),x)) holds
(ProjPMap1 ((chi (A,[:X1,X2:])),x)) . y = (chi ((Measurable-X-section (A,x)),X2)) . y

let y be Element of X2; :: thesis: ( y in dom (ProjPMap1 ((chi (A,[:X1,X2:])),x)) implies (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . b₁ = (chi ((Measurable-X-section (A,x)),X2)) . b₁ )
assume y in dom (ProjPMap1 ((chi (A,[:X1,X2:])),x)) ; :: thesis: (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . b₁ = (chi ((Measurable-X-section (A,x)),X2)) . b₁
A3: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
then [x,y] in dom (chi (A,[:X1,X2:])) by FUNCT_3:def 3;
then A4: (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . y = (chi (A,[:X1,X2:])) . (x,y) by Def3;
A5: Measurable-X-section (A,x) = X-section (A,x) by MEASUR11:def 6
.= { y where y is Element of X2 : [x,y] in A } by MEASUR11:def 4 ;

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

suppose A6: [x,y] in A ; :: thesis: (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . b₁ = (chi ((Measurable-X-section (A,x)),X2)) . b₁

then y in Measurable-X-section (A,x) by A5;
then (chi ((Measurable-X-section (A,x)),X2)) . y = 1 by FUNCT_3:def 3;
hence (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . y = (chi ((Measurable-X-section (A,x)),X2)) . y by A4, A6, FUNCT_3:def 3; :: thesis: verum

end;

suppose A7: not [x,y] in A ; :: thesis: (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . b₁ = (chi ((Measurable-X-section (A,x)),X2)) . b₁

now :: thesis: not y in Measurable-X-section (A,x)

assume y in Measurable-X-section (A,x) ; :: thesis: contradiction
then ex y1 being Element of X2 st
( y1 = y & [x,y1] in A ) by A5;
hence contradiction by A7; :: thesis: verum

end;

then (chi ((Measurable-X-section (A,x)),X2)) . y = 0 by FUNCT_3:def 3;
hence (ProjPMap1 ((chi (A,[:X1,X2:])),x)) . y = (chi ((Measurable-X-section (A,x)),X2)) . y by A3, A4, A7, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

hence ProjPMap1 ((chi (A,[:X1,X2:])),x) = chi ((Measurable-X-section (A,x)),X2) by A2, PARTFUN1:5; :: thesis: ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1)
A8: ( y in XX2 implies Y-section ([:XX1,XX2:],y) = XX1 ) by MEASUR11:22;
dom (ProjPMap2 ((chi (A,[:X1,X2:])),y)) = Y-section ((dom (chi (A,[:X1,X2:]))),y) by Def4
.= Y-section (XX12,y) by FUNCT_3:def 3 ;
then A9: dom (ProjPMap2 ((chi (A,[:X1,X2:])),y)) = dom (chi ((Measurable-Y-section (A,y)),X1)) by A8, FUNCT_3:def 3;

now :: thesis: for x being Element of X1 st x in dom (ProjPMap2 ((chi (A,[:X1,X2:])),y)) holds
(ProjPMap2 ((chi (A,[:X1,X2:])),y)) . x = (chi ((Measurable-Y-section (A,y)),X1)) . x

let x be Element of X1; :: thesis: ( x in dom (ProjPMap2 ((chi (A,[:X1,X2:])),y)) implies (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . b₁ = (chi ((Measurable-Y-section (A,y)),X1)) . b₁ )
assume x in dom (ProjPMap2 ((chi (A,[:X1,X2:])),y)) ; :: thesis: (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . b₁ = (chi ((Measurable-Y-section (A,y)),X1)) . b₁
A10: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
then [x,y] in dom (chi (A,[:X1,X2:])) by FUNCT_3:def 3;
then A11: (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . x = (chi (A,[:X1,X2:])) . (x,y) by Def4;
A12: Measurable-Y-section (A,y) = Y-section (A,y) by MEASUR11:def 7
.= { x where x is Element of X1 : [x,y] in A } by MEASUR11:def 5 ;

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

suppose A13: [x,y] in A ; :: thesis: (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . b₁ = (chi ((Measurable-Y-section (A,y)),X1)) . b₁

then x in Measurable-Y-section (A,y) by A12;
then (chi ((Measurable-Y-section (A,y)),X1)) . x = 1 by FUNCT_3:def 3;
hence (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . x = (chi ((Measurable-Y-section (A,y)),X1)) . x by A11, A13, FUNCT_3:def 3; :: thesis: verum

end;

suppose A14: not [x,y] in A ; :: thesis: (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . b₁ = (chi ((Measurable-Y-section (A,y)),X1)) . b₁

now :: thesis: not x in Measurable-Y-section (A,y)

assume x in Measurable-Y-section (A,y) ; :: thesis: contradiction
then ex x1 being Element of X1 st
( x1 = x & [x1,y] in A ) by A12;
hence contradiction by A14; :: thesis: verum

end;

then (chi ((Measurable-Y-section (A,y)),X1)) . x = 0 by FUNCT_3:def 3;
hence (ProjPMap2 ((chi (A,[:X1,X2:])),y)) . x = (chi ((Measurable-Y-section (A,y)),X1)) . x by A10, A11, A14, FUNCT_3:def 3; :: thesis: verum

end;

end;

end;

hence ProjPMap2 ((chi (A,[:X1,X2:])),y) = chi ((Measurable-Y-section (A,y)),X1) by A9, PARTFUN1:5; :: thesis: verum