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, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
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, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let M2 be sigma_Measure of S2; :: thesis: for E, A, B being Element of sigma (measurable_rectangles (S1,S2))
for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let E, A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st E = dom f & f is nonnegative & f is E -measurable & A misses B holds
( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( E = dom f & f is nonnegative & f is E -measurable & A misses B implies ( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) ) )
assume that
A1: E = dom f and
A2: f is nonnegative and
A3: f is E -measurable and
A4: A misses B ; :: thesis: ( Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) & Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) )
Integral1 (M1,(f | A)) is nonnegative by A1, A2, A3, Th66;
then reconsider IA = Integral1 (M1,(f | A)) as without-infty Function of X2,ExtREAL ;
Integral1 (M1,(f | B)) is nonnegative by A1, A2, A3, Th66;
then reconsider IB = Integral1 (M1,(f | B)) as without-infty Function of X2,ExtREAL ;

now :: thesis: for y being Element of X2 holds (Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . y

let y be Element of X2; :: thesis: (Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . y
A5: ( Y-section (A,y) = Measurable-Y-section (A,y) & Y-section (B,y) = Measurable-Y-section (B,y) & Y-section ((A \/ B),y) = Measurable-Y-section ((A \/ B),y) ) by MEASUR11:def 7;
A6: dom (ProjPMap2 (f,y)) = Y-section (E,y) by A1, Def4
.= Measurable-Y-section (E,y) by MEASUR11:def 7 ;
A7: ProjPMap2 (f,y) is Measurable-Y-section (E,y) -measurable by A1, A3, Th47;
A /\ B = {} [:X1,X2:] by A4;
then Y-section ((A /\ B),y) = {} by MEASUR11:24;
then A8: Measurable-Y-section (A,y) misses Measurable-Y-section (B,y) by A5, MEASUR11:27;
( ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Y-section (A,y)) & ProjPMap2 ((f | B),y) = (ProjPMap2 (f,y)) | (Y-section (B,y)) ) by Th34;
then A9: ( ProjPMap2 ((f | A),y) = (ProjPMap2 (f,y)) | (Measurable-Y-section (A,y)) & ProjPMap2 ((f | B),y) = (ProjPMap2 (f,y)) | (Measurable-Y-section (B,y)) ) by MEASUR11:def 7;
A10: (Measurable-Y-section (A,y)) \/ (Measurable-Y-section (B,y)) = Measurable-Y-section ((A \/ B),y) by A5, MEASUR11:26;
(IA + IB) . y = ((Integral1 (M1,(f | A))) . y) + ((Integral1 (M1,(f | B))) . y) by DBLSEQ_3:7
.= (Integral (M1,(ProjPMap2 ((f | A),y)))) + ((Integral1 (M1,(f | B))) . y) by Def7
.= (Integral (M1,(ProjPMap2 ((f | A),y)))) + (Integral (M1,(ProjPMap2 ((f | B),y)))) by Def7
.= Integral (M1,((ProjPMap2 (f,y)) | (Measurable-Y-section ((A \/ B),y)))) by A2, A6, A7, A8, A9, A10, Th32, MESFUNC5:91
.= Integral (M1,((ProjPMap2 (f,y)) | (Y-section ((A \/ B),y)))) by MEASUR11:def 7
.= Integral (M1,(ProjPMap2 ((f | (A \/ B)),y))) by Th34 ;
hence (Integral1 (M1,(f | (A \/ B)))) . y = (IA + IB) . y by Def7; :: thesis: verum

end;

hence Integral1 (M1,(f | (A \/ B))) = (Integral1 (M1,(f | A))) + (Integral1 (M1,(f | B))) by FUNCT_2:def 8; :: thesis: Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B)))
Integral2 (M2,(f | A)) is nonnegative by A1, A2, A3, Th66;
then reconsider JA = Integral2 (M2,(f | A)) as without-infty Function of X1,ExtREAL ;
Integral2 (M2,(f | B)) is nonnegative by A1, A2, A3, Th66;
then reconsider JB = Integral2 (M2,(f | B)) as without-infty Function of X1,ExtREAL ;

now :: thesis: for x being Element of X1 holds (Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . x

let x be Element of X1; :: thesis: (Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . x
A11: ( X-section (A,x) = Measurable-X-section (A,x) & X-section (B,x) = Measurable-X-section (B,x) & X-section ((A \/ B),x) = Measurable-X-section ((A \/ B),x) ) by MEASUR11:def 6;
A12: dom (ProjPMap1 (f,x)) = X-section (E,x) by A1, Def3
.= Measurable-X-section (E,x) by MEASUR11:def 6 ;
A13: ProjPMap1 (f,x) is Measurable-X-section (E,x) -measurable by A1, A3, Th47;
A /\ B = {} [:X1,X2:] by A4;
then X-section ((A /\ B),x) = {} by MEASUR11:24;
then A14: Measurable-X-section (A,x) misses Measurable-X-section (B,x) by A11, MEASUR11:27;
( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (X-section (A,x)) & ProjPMap1 ((f | B),x) = (ProjPMap1 (f,x)) | (X-section (B,x)) ) by Th34;
then A15: ( ProjPMap1 ((f | A),x) = (ProjPMap1 (f,x)) | (Measurable-X-section (A,x)) & ProjPMap1 ((f | B),x) = (ProjPMap1 (f,x)) | (Measurable-X-section (B,x)) ) by MEASUR11:def 6;
A16: (Measurable-X-section (A,x)) \/ (Measurable-X-section (B,x)) = Measurable-X-section ((A \/ B),x) by A11, MEASUR11:26;
(JA + JB) . x = ((Integral2 (M2,(f | A))) . x) + ((Integral2 (M2,(f | B))) . x) by DBLSEQ_3:7
.= (Integral (M2,(ProjPMap1 ((f | A),x)))) + ((Integral2 (M2,(f | B))) . x) by Def8
.= (Integral (M2,(ProjPMap1 ((f | A),x)))) + (Integral (M2,(ProjPMap1 ((f | B),x)))) by Def8
.= Integral (M2,((ProjPMap1 (f,x)) | (Measurable-X-section ((A \/ B),x)))) by A2, A12, A13, A14, A15, A16, Th32, MESFUNC5:91
.= Integral (M2,((ProjPMap1 (f,x)) | (X-section ((A \/ B),x)))) by MEASUR11:def 6
.= Integral (M2,(ProjPMap1 ((f | (A \/ B)),x))) by Th34 ;
hence (Integral2 (M2,(f | (A \/ B)))) . x = (JA + JB) . x by Def8; :: thesis: verum

end;

hence Integral2 (M2,(f | (A \/ B))) = (Integral2 (M2,(f | A))) + (Integral2 (M2,(f | B))) by FUNCT_2:def 8; :: thesis: verum