let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & ex B being Element of S st
( B = dom g & g is B -measurable ) & f is nonnegative & g is nonnegative holds
ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & ex B being Element of S st
( B = dom g & g is B -measurable ) & f is nonnegative & g is nonnegative holds
ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st
( A = dom f & f is A -measurable ) & ex B being Element of S st
( B = dom g & g is B -measurable ) & f is nonnegative & g is nonnegative holds
ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st
( A = dom f & f is A -measurable ) & ex B being Element of S st
( B = dom g & g is B -measurable ) & f is nonnegative & g is nonnegative implies ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) ) )
assume that
A1: ex A being Element of S st
( A = dom f & f is A -measurable ) and
A2: ex B being Element of S st
( B = dom g & g is B -measurable ) and
A3: f is nonnegative and
A4: g is nonnegative ; :: thesis: ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
set g1 = g | ((dom f) /\ (dom g));
A5: g | ((dom f) /\ (dom g)) is () by A4, Th12, Th15;
A6: g | ((dom f) /\ (dom g)) is nonnegative by A4, Th15;
dom (g | ((dom f) /\ (dom g))) = (dom g) /\ ((dom f) /\ (dom g)) by RELAT_1:61;
then A7: dom (g | ((dom f) /\ (dom g))) = ((dom g) /\ (dom g)) /\ (dom f) by XBOOLE_1:16;
consider B being Element of S such that
A8: B = dom g and
A9: g is B -measurable by A2;
consider A being Element of S such that
A10: A = dom f and
A11: f is A -measurable by A1;
take C = A /\ B; :: thesis: ( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) )
A12: C = dom (f + g) by A3, A4, A10, A8, Th16;
A13: C = (dom g) /\ C by A8, XBOOLE_1:17, XBOOLE_1:28;
g is C -measurable by A9, MESFUNC1:30, XBOOLE_1:17;
then A14: g | C is C -measurable by A13, Th42;
A15: C = (dom f) /\ C by A10, XBOOLE_1:17, XBOOLE_1:28;
f is C -measurable by A11, MESFUNC1:30, XBOOLE_1:17;
then A16: f | C is C -measurable by A15, Th42;
set f1 = f | ((dom f) /\ (dom g));
dom (f | ((dom f) /\ (dom g))) = (dom f) /\ ((dom f) /\ (dom g)) by RELAT_1:61;
then A17: dom (f | ((dom f) /\ (dom g))) = ((dom f) /\ (dom f)) /\ (dom g) by XBOOLE_1:16;
A18: f | ((dom f) /\ (dom g)) is () by A3, Th12, Th15;
then A19: dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) = C /\ C by A10, A8, A17, A7, A5, Th16;
A20: dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) = (dom (f | ((dom f) /\ (dom g)))) /\ (dom (g | ((dom f) /\ (dom g)))) by A18, A5, Th16;
A21: for x being object st x in dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) holds
((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = (f + g) . x

proof

let x be object ; :: thesis: ( x in dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) implies ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = (f + g) . x )
assume A22: x in dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) ; :: thesis: ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = (f + g) . x
then A23: x in dom (f | ((dom f) /\ (dom g))) by A20, XBOOLE_0:def 4;
A24: x in dom (g | ((dom f) /\ (dom g))) by A20, A22, XBOOLE_0:def 4;
((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = ((f | ((dom f) /\ (dom g))) . x) + ((g | ((dom f) /\ (dom g))) . x) by A22, MESFUNC1:def 3
.= (f . x) + ((g | ((dom f) /\ (dom g))) . x) by A23, FUNCT_1:47
.= (f . x) + (g . x) by A24, FUNCT_1:47 ;
hence ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = (f + g) . x by A12, A19, A22, MESFUNC1:def 3; :: thesis: verum

end;

f | ((dom f) /\ (dom g)) is nonnegative by A3, Th15;
then integral+ (M,((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g))))) = (integral+ (M,(f | ((dom f) /\ (dom g))))) + (integral+ (M,(g | ((dom f) /\ (dom g))))) by A10, A8, A17, A7, A16, A14, A6, Lm10;
hence ( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) ) by A10, A8, A12, A19, A21, FUNCT_1:2; :: thesis: verum