let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let A be Element of S1; :: thesis:
let B be Element of S2; :: thesis:
let x be Element of X1; :: thesis:
set CAB = (chi ([:A,B:],[:X1,X2:])) | E;
ProjPMap1 ((chi ([:A,B:],[:X1,X2:])),x) = ProjMap1 ((chi ([:A,B:],[:X1,X2:])),x) by Th27;
then A0: dom (ProjPMap1 ((chi ([:A,B:],[:X1,X2:])),x)) = X2 by FUNCT_2:def 1;
ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x) = (ProjPMap1 ((chi ([:A,B:],[:X1,X2:])),x)) | (X-section (E,x)) by Th34;
then dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) = X2 /\ (X-section (E,x)) by A0, RELAT_1:61;
then A1: dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) = X-section (E,x) by XBOOLE_1:28;
A2: for y being Element of X2 holds (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (((chi (A,X1)) | (Measurable-Y-section (E,y))) . x) * ((chi (B,X2)) . y)

let y be Element of X2; :: thesis:

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

suppose A3: [x,y] in E ; :: thesis:

then y in X-section (E,x) by Th25;
then (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = ((chi ([:A,B:],[:X1,X2:])) | E) . (x,y) by A1, Th26;
then A4: (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (chi ([:A,B:],[:X1,X2:])) . (x,y) by A3, FUNCT_1:49;
x in Y-section (E,y) by A3, Th25;
then x in Measurable-Y-section (E,y) by MEASUR11:def 7;
then ((chi (A,X1)) | (Measurable-Y-section (E,y))) . x = (chi (A,X1)) . x by FUNCT_1:49;
hence (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (((chi (A,X1)) | (Measurable-Y-section (E,y))) . x) * ((chi (B,X2)) . y) by A4, MEASUR10:2; :: thesis:

end;

suppose A5: not [x,y] in E ; :: thesis:

then not y in X-section (E,x) by Th25;
then A6: (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = 0 by A1, FUNCT_1:def 2;
not x in Y-section (E,y) by A5, Th25;
then not x in Measurable-Y-section (E,y) by MEASUR11:def 7;
then not x in dom ((chi (A,X1)) | (Measurable-Y-section (E,y))) by Th18;
then ((chi (A,X1)) | (Measurable-Y-section (E,y))) . x = 0 by FUNCT_1:def 2;
hence (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (((chi (A,X1)) | (Measurable-Y-section (E,y))) . x) * ((chi (B,X2)) . y) by A6; :: thesis:

end;

end;

end;

suppose x in A ; :: thesis:

then A7: (chi (A,X1)) . x = 1 by FUNCT_3:def 3;
then A8: (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = M2 . (B /\ (Measurable-X-section (E,x))) by XXREAL_3:81;
dom ((chi (B,X2)) | (Measurable-X-section (E,x))) = Measurable-X-section (E,x) by Th18;
then A9: dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) = dom ((chi (B,X2)) | (Measurable-X-section (E,x))) by A1, MEASUR11:def 6;
for y being Element of X2 st y in dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) holds
(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = ((chi (B,X2)) | (Measurable-X-section (E,x))) . y

let y be Element of X2; :: thesis:
assume A10: y in dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) ; :: thesis:
then A11: y in Measurable-X-section (E,x) by A1, MEASUR11:def 6;
[x,y] in E by A1, A10, Th25;
then x in Y-section (E,y) by Th25;
then x in Measurable-Y-section (E,y) by MEASUR11:def 7;
then A12: ((chi (A,X1)) | (Measurable-Y-section (E,y))) . x = (chi (A,X1)) . x by FUNCT_1:49;
(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (((chi (A,X1)) | (Measurable-Y-section (E,y))) . x) * ((chi (B,X2)) . y) by A2;
then (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (chi (B,X2)) . y by A7, A12, XXREAL_3:81;
hence (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = ((chi (B,X2)) | (Measurable-X-section (E,x))) . y by A11, FUNCT_1:49; :: thesis:

end;

then ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x) = (chi (B,X2)) | (Measurable-X-section (E,x)) by A9, PARTFUN1:5;
hence (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x))) by A8, Th20; :: thesis:

end;

suppose not x in A ; :: thesis:

then A13: (chi (A,X1)) . x = 0 by FUNCT_3:def 3;
then A14: (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = 0 ;
A15: {} is Element of S2 by PROB_1:4;
A16: dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) = Measurable-X-section (E,x) by A1, MEASUR11:def 6
.= dom ((chi ({},X2)) | (Measurable-X-section (E,x))) by Th18 ;
for y being Element of X2 st y in dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) holds
(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = ((chi ({},X2)) | (Measurable-X-section (E,x))) . y

let y be Element of X2; :: thesis:
assume A17: y in dom (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) ; :: thesis:
then y in Measurable-X-section (E,x) by A1, MEASUR11:def 6;
then A18: ((chi ({},X2)) | (Measurable-X-section (E,x))) . y = (chi ({},X2)) . y by FUNCT_1:49;
[x,y] in E by A1, A17, Th25;
then x in Y-section (E,y) by Th25;
then x in Measurable-Y-section (E,y) by MEASUR11:def 7;
then A19: ((chi (A,X1)) | (Measurable-Y-section (E,y))) . x = (chi (A,X1)) . x by FUNCT_1:49;
(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = (((chi (A,X1)) | (Measurable-Y-section (E,y))) . x) * ((chi (B,X2)) . y) by A2;
then (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = 0 by A13, A19;
hence (ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x)) . y = ((chi ({},X2)) | (Measurable-X-section (E,x))) . y by A18, FUNCT_3:def 3; :: thesis:

end;

then ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x) = (chi ({},X2)) | (Measurable-X-section (E,x)) by A16, PARTFUN1:5;
then Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x))) = M2 . ({} /\ (Measurable-X-section (E,x))) by A15, Th20;
hence (M2 . (B /\ (Measurable-X-section (E,x)))) * ((chi (A,X1)) . x) = Integral (M2,(ProjPMap1 (((chi ([:A,B:],[:X1,X2:])) | E),x))) by A14, VALUED_0:def 19; :: thesis:

end;

end;