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 M1 be sigma_Measure of S1; :: thesis:
let A be Element of S1; :: thesis:
let B be Element of S2; :: thesis:
let y be Element of X2; :: thesis:
set CAB = (chi ([:A,B:],[:X1,X2:])) | E;
ProjPMap2 ((chi ([:A,B:],[:X1,X2:])),y) = ProjMap2 ((chi ([:A,B:],[:X1,X2:])),y) by Th27;
then A0: dom (ProjPMap2 ((chi ([:A,B:],[:X1,X2:])),y)) = X1 by FUNCT_2:def 1;
ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y) = (ProjPMap2 ((chi ([:A,B:],[:X1,X2:])),y)) | (Y-section (E,y)) by Th34;
then dom (ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)) = X1 /\ (Y-section (E,y)) by A0, RELAT_1:61;
then A1: dom (ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)) = Y-section (E,y) by XBOOLE_1:28;
A2: for x being Element of X1 holds (ProjPMap2 (((chi ([:A,B:],[:X1,X2:])) | E),y)) . x = (((chi (B,X2)) | (Measurable-X-section (E,x))) . y) * ((chi (A,X1)) . x)

let x be Element of X1; :: thesis:

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

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

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

end;

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

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

end;

end;

end;

suppose y in B ; :: thesis:

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

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

end;

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

end;

suppose not y in B ; :: thesis:

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

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

end;

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

end;

end;