let X1, X2 be non empty set ; :: thesis:
let S1 be SigmaField of X1; :: thesis:
let S2 be SigmaField of X2; :: thesis:
let M1 be sigma_Measure of S1; :: thesis:
let M2 be sigma_Measure of S2; :: thesis:
let f, g be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
let A, B be Element of sigma (measurable_rectangles (S1,S2)); :: thesis:
assume that
A1: A = dom f and
A2: f is nonnegative and
A3: f is A -measurable and
A4: B = dom g and
A5: g is nonnegative and
A6: g is B -measurable ; :: thesis:
A7: dom (f + g) = A /\ B by A1, A2, A4, A5, MESFUNC5:22;
set f1 = f | (A /\ B);
set g1 = g | (A /\ B);
A8: ( dom (f | (A /\ B)) = A /\ B & dom (g | (A /\ B)) = A /\ B ) by A1, A4, XBOOLE_1:17, RELAT_1:62;
A9: ( (dom f) /\ (A /\ B) = A /\ B & (dom g) /\ (A /\ B) = A /\ B ) by A1, A4, XBOOLE_1:17, XBOOLE_1:28;
A10: ( f is A /\ B -measurable & g is A /\ B -measurable ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
then A11: ( f | (A /\ B) is A /\ B -measurable & g | (A /\ B) is A /\ B -measurable ) by A9, MESFUNC5:42;
A12: ( f | (A /\ B) is nonnegative & g | (A /\ B) is nonnegative ) by A2, A5, MESFUNC5:15;
then A13: ( Integral1 (M1,(f | (A /\ B))) is V112() & Integral1 (M1,(g | (A /\ B))) is V112() & Integral2 (M2,(f | (A /\ B))) is V112() & Integral2 (M2,(g | (A /\ B))) is V112() ) by A8, A11, Th66;
then reconsider IF1 = Integral1 (M1,(f | (A /\ B))), IG1 = Integral1 (M1,(g | (A /\ B))) as V120() Function of X2,ExtREAL ;
reconsider IF2 = Integral2 (M2,(f | (A /\ B))), IG2 = Integral2 (M2,(g | (A /\ B))) as V120() Function of X1,ExtREAL by A13;
A14: ( IF1 + IG1 = (Integral1 (M1,(f | (A /\ B)))) + (Integral1 (M1,(g | (A /\ B)))) & IF2 + IG2 = (Integral2 (M2,(f | (A /\ B)))) + (Integral2 (M2,(g | (A /\ B)))) ) ;
A21: f + g is nonnegative by A2, A5, MESFUNC5:22;
for y being Element of X2 holds ((Integral1 (M1,(f | (A /\ B)))) + (Integral1 (M1,(g | (A /\ B))))) . y = (Integral1 (M1,(f + g))) . y

let y be Element of X2; :: thesis:
( dom (ProjPMap2 ((f | (A /\ B)),y)) = Y-section ((A /\ B),y) & dom (ProjPMap2 ((g | (A /\ B)),y)) = Y-section ((A /\ B),y) ) by A8, Def4;
then A15: ( dom (ProjPMap2 ((f | (A /\ B)),y)) = Measurable-Y-section ((A /\ B),y) & dom (ProjPMap2 ((g | (A /\ B)),y)) = Measurable-Y-section ((A /\ B),y) ) by MEASUR11:def 7;
( ProjPMap2 ((f | (A /\ B)),y) is Measurable-Y-section ((A /\ B),y) -measurable & ProjPMap2 ((g | (A /\ B)),y) is Measurable-Y-section ((A /\ B),y) -measurable ) by A8, A11, Th47;
then A16: ( Integral (M1,(ProjPMap2 ((f | (A /\ B)),y))) = integral+ (M1,(ProjPMap2 ((f | (A /\ B)),y))) & Integral (M1,(ProjPMap2 ((g | (A /\ B)),y))) = integral+ (M1,(ProjPMap2 ((g | (A /\ B)),y))) ) by A12, A15, Th32, MESFUNC5:88;
A17: ProjPMap2 ((f + g),y) = (ProjPMap2 (f,y)) + (ProjPMap2 (g,y)) by Th44;
( ProjPMap2 ((f | (A /\ B)),y) = (ProjPMap2 (f,y)) | (Y-section ((A /\ B),y)) & ProjPMap2 ((g | (A /\ B)),y) = (ProjPMap2 (g,y)) | (Y-section ((A /\ B),y)) ) by Th34;
then A18: ( ProjPMap2 ((f | (A /\ B)),y) = (ProjPMap2 (f,y)) | (Measurable-Y-section ((A /\ B),y)) & ProjPMap2 ((g | (A /\ B)),y) = (ProjPMap2 (g,y)) | (Measurable-Y-section ((A /\ B),y)) ) by MEASUR11:def 7;
( dom (ProjPMap2 (f,y)) = Y-section (A,y) & dom (ProjPMap2 (g,y)) = Y-section (B,y) ) by A1, A4, Def4;
then A19: ( dom (ProjPMap2 (f,y)) = Measurable-Y-section (A,y) & dom (ProjPMap2 (g,y)) = Measurable-Y-section (B,y) ) by MEASUR11:def 7;
dom (ProjPMap2 ((f + g),y)) = Y-section ((A /\ B),y) by A7, Def4;
then A20: Measurable-Y-section ((A /\ B),y) = dom (ProjPMap2 ((f + g),y)) by MEASUR11:def 7;
f + g is A /\ B -measurable by A2, A5, A10, MESFUNC5:31;
then A22: ProjPMap2 ((f + g),y) is Measurable-Y-section ((A /\ B),y) -measurable by A7, Th47;
A23: ((Integral1 (M1,(f | (A /\ B)))) + (Integral1 (M1,(g | (A /\ B))))) . y = ((Integral1 (M1,(f | (A /\ B)))) . y) + ((Integral1 (M1,(g | (A /\ B)))) . y) by A13, DBLSEQ_3:7
.= (Integral (M1,(ProjPMap2 ((f | (A /\ B)),y)))) + ((Integral1 (M1,(g | (A /\ B)))) . y) by Def7
.= (integral+ (M1,(ProjPMap2 ((f | (A /\ B)),y)))) + (integral+ (M1,(ProjPMap2 ((g | (A /\ B)),y)))) by A16, Def7 ;
( ProjPMap2 (f,y) is nonnegative & ProjPMap2 (g,y) is nonnegative & ProjPMap2 (f,y) is Measurable-Y-section (A,y) -measurable & ProjPMap2 (g,y) is Measurable-Y-section (B,y) -measurable ) by A1, A3, A4, A6, A2, A5, Th32, Th47;
then ex C being Element of S1 st
( C = dom ((ProjPMap2 (f,y)) + (ProjPMap2 (g,y))) & integral+ (M1,((ProjPMap2 (f,y)) + (ProjPMap2 (g,y)))) = (integral+ (M1,((ProjPMap2 (f,y)) | C))) + (integral+ (M1,((ProjPMap2 (g,y)) | C))) ) by A19, MESFUNC5:78;
then ((Integral1 (M1,(f | (A /\ B)))) + (Integral1 (M1,(g | (A /\ B))))) . y = Integral (M1,(ProjPMap2 ((f + g),y))) by A17, A18, A20, A23, A21, A22, Th32, MESFUNC5:88;
hence (Integral1 (M1,(f + g))) . y = ((Integral1 (M1,(f | (A /\ B)))) + (Integral1 (M1,(g | (A /\ B))))) . y by Def7; :: thesis:

end;

hence Integral1 (M1,(f + g)) = (Integral1 (M1,(f | (dom (f + g))))) + (Integral1 (M1,(g | (dom (f + g))))) by A7, A14, FUNCT_2:63; :: thesis:
for x being Element of X1 holds ((Integral2 (M2,(f | (A /\ B)))) + (Integral2 (M2,(g | (A /\ B))))) . x = (Integral2 (M2,(f + g))) . x

let x be Element of X1; :: thesis:
( dom (ProjPMap1 ((f | (A /\ B)),x)) = X-section ((A /\ B),x) & dom (ProjPMap1 ((g | (A /\ B)),x)) = X-section ((A /\ B),x) ) by A8, Def3;
then B15: ( dom (ProjPMap1 ((f | (A /\ B)),x)) = Measurable-X-section ((A /\ B),x) & dom (ProjPMap1 ((g | (A /\ B)),x)) = Measurable-X-section ((A /\ B),x) ) by MEASUR11:def 6;
( ProjPMap1 ((f | (A /\ B)),x) is Measurable-X-section ((A /\ B),x) -measurable & ProjPMap1 ((g | (A /\ B)),x) is Measurable-X-section ((A /\ B),x) -measurable ) by A8, A11, Th47;
then B16: ( Integral (M2,(ProjPMap1 ((f | (A /\ B)),x))) = integral+ (M2,(ProjPMap1 ((f | (A /\ B)),x))) & Integral (M2,(ProjPMap1 ((g | (A /\ B)),x))) = integral+ (M2,(ProjPMap1 ((g | (A /\ B)),x))) ) by A12, B15, Th32, MESFUNC5:88;
B17: ProjPMap1 ((f + g),x) = (ProjPMap1 (f,x)) + (ProjPMap1 (g,x)) by Th44;
( ProjPMap1 ((f | (A /\ B)),x) = (ProjPMap1 (f,x)) | (X-section ((A /\ B),x)) & ProjPMap1 ((g | (A /\ B)),x) = (ProjPMap1 (g,x)) | (X-section ((A /\ B),x)) ) by Th34;
then B18: ( ProjPMap1 ((f | (A /\ B)),x) = (ProjPMap1 (f,x)) | (Measurable-X-section ((A /\ B),x)) & ProjPMap1 ((g | (A /\ B)),x) = (ProjPMap1 (g,x)) | (Measurable-X-section ((A /\ B),x)) ) by MEASUR11:def 6;
( dom (ProjPMap1 (f,x)) = X-section (A,x) & dom (ProjPMap1 (g,x)) = X-section (B,x) ) by A1, A4, Def3;
then B19: ( dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) & dom (ProjPMap1 (g,x)) = Measurable-X-section (B,x) ) by MEASUR11:def 6;
dom (ProjPMap1 ((f + g),x)) = X-section ((A /\ B),x) by A7, Def3;
then B20: Measurable-X-section ((A /\ B),x) = dom (ProjPMap1 ((f + g),x)) by MEASUR11:def 6;
f + g is A /\ B -measurable by A2, A5, A10, MESFUNC5:31;
then B22: ProjPMap1 ((f + g),x) is Measurable-X-section ((A /\ B),x) -measurable by A7, Th47;
B23: ((Integral2 (M2,(f | (A /\ B)))) + (Integral2 (M2,(g | (A /\ B))))) . x = ((Integral2 (M2,(f | (A /\ B)))) . x) + ((Integral2 (M2,(g | (A /\ B)))) . x) by A13, DBLSEQ_3:7
.= (Integral (M2,(ProjPMap1 ((f | (A /\ B)),x)))) + ((Integral2 (M2,(g | (A /\ B)))) . x) by Def8
.= (integral+ (M2,(ProjPMap1 ((f | (A /\ B)),x)))) + (integral+ (M2,(ProjPMap1 ((g | (A /\ B)),x)))) by B16, Def8 ;
( ProjPMap1 (f,x) is nonnegative & ProjPMap1 (g,x) is nonnegative & ProjPMap1 (f,x) is Measurable-X-section (A,x) -measurable & ProjPMap1 (g,x) is Measurable-X-section (B,x) -measurable ) by A1, A3, A4, A6, A2, A5, Th32, Th47;
then ex C being Element of S2 st
( C = dom ((ProjPMap1 (f,x)) + (ProjPMap1 (g,x))) & integral+ (M2,((ProjPMap1 (f,x)) + (ProjPMap1 (g,x)))) = (integral+ (M2,((ProjPMap1 (f,x)) | C))) + (integral+ (M2,((ProjPMap1 (g,x)) | C))) ) by B19, MESFUNC5:78;
then ((Integral2 (M2,(f | (A /\ B)))) + (Integral2 (M2,(g | (A /\ B))))) . x = Integral (M2,(ProjPMap1 ((f + g),x))) by B17, B18, B20, B23, A21, B22, Th32, MESFUNC5:88;
hence (Integral2 (M2,(f + g))) . x = ((Integral2 (M2,(f | (A /\ B)))) + (Integral2 (M2,(g | (A /\ B))))) . x by Def8; :: thesis:

end;

hence Integral2 (M2,(f + g)) = (Integral2 (M2,(f | (dom (f + g))))) + (Integral2 (M2,(g | (dom (f + g))))) by A7, A14, FUNCT_2:63; :: thesis: