let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let er be ExtReal; :: thesis: ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider C = (chi (E,[:X1,X2:])) | E as PartFunc of [:X1,X2:],ExtREAL ;

per cases ( er in REAL or er = +infty or er = -infty ) by XXREAL_0:14;

suppose er in REAL ; :: thesis: ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )

then reconsider r = er as Real ;
A1: chi (r,E,[:X1,X2:]) = r (#) (chi (E,[:X1,X2:])) by Th1;
A2: chi (E,[:X1,X2:]) is XX12 -measurable by MESFUNC2:29;
A3: dom (chi (E,[:X1,X2:])) = XX12 by FUNCT_2:def 1;
A4: dom ((chi (E,[:X1,X2:])) | E) = (dom (chi (E,[:X1,X2:]))) /\ E by RELAT_1:61
.= [:X1,X2:] /\ E by FUNCT_2:def 1
.= E by XBOOLE_1:28 ;
A5: (chi (E,[:X1,X2:])) | E is nonnegative by MESFUNC5:15;
E = (dom (chi (E,[:X1,X2:]))) /\ E by A3, XBOOLE_1:28;
then A6: (chi (E,[:X1,X2:])) | E is E -measurable by MESFUNC2:29, MESFUNC5:42;
Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)) = Integral1 (M1,(r (#) C)) by A1, MESFUN11:2
.= r (#) (Integral1 (M1,C)) by A4, A5, A6, Th78
.= r (#) (Integral1 (M1,(chi (E,[:X1,X2:])))) by Th79
.= Integral1 (M1,(r (#) (chi (E,[:X1,X2:])))) by A2, A3, Th78 ;
hence Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) by Th1; :: thesis: Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:])))
Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)) = Integral2 (M2,(r (#) C)) by A1, MESFUN11:2
.= r (#) (Integral2 (M2,C)) by A4, A5, A6, Th78
.= r (#) (Integral2 (M2,(chi (E,[:X1,X2:])))) by Th79
.= Integral2 (M2,(r (#) (chi (E,[:X1,X2:])))) by A2, A3, Th78 ;
hence Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) by Th1; :: thesis: verum

end;

suppose er = +infty ; :: thesis: ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )

then chi (er,E,[:X1,X2:]) = Xchi (E,[:X1,X2:]) by Th2;
hence ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) ) by Th80; :: thesis: verum

end;

suppose d0: er = -infty ; :: thesis: ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )

reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider XE = (Xchi (E,[:X1,X2:])) | E as PartFunc of [:X1,X2:],ExtREAL ;
d3: Xchi (E,[:X1,X2:]) is XX12 -measurable by MEASUR10:32;
e2: XE is nonnegative by MESFUNC5:15;
d4: dom (Xchi (E,[:X1,X2:])) = XX12 by FUNCT_2:def 1;
then e1: dom XE = E by RELAT_1:62;
then E = (dom (Xchi (E,[:X1,X2:]))) /\ E by RELAT_1:61;
then e3: XE is E -measurable by MESFUNC5:42;
d1: chi (er,E,[:X1,X2:]) = - (Xchi (E,[:X1,X2:])) by d0, Th2
.= (- 1) (#) (Xchi (E,[:X1,X2:])) by MESFUNC2:9 ;
Integral1 (M1,(chi (er,E,[:X1,X2:]))) = (- 1) (#) (Integral1 (M1,(Xchi (E,[:X1,X2:])))) by d1, d3, d4, Th78
.= (- 1) (#) (Integral1 (M1,((Xchi (E,[:X1,X2:])) | E))) by Th80
.= Integral1 (M1,((- 1) (#) XE)) by e1, e2, e3, Th78
.= Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) by d1, MESFUN11:2 ;
hence Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) ; :: thesis: Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:])))
Integral2 (M2,(chi (er,E,[:X1,X2:]))) = (- 1) (#) (Integral2 (M2,(Xchi (E,[:X1,X2:])))) by d1, d3, d4, Th78
.= (- 1) (#) (Integral2 (M2,((Xchi (E,[:X1,X2:])) | E))) by Th80
.= Integral2 (M2,((- 1) (#) XE)) by e1, e2, e3, Th78
.= Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) by d1, MESFUN11:2 ;
hence Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) ; :: thesis: verum

end;

end;