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_measurable_on A ) & ex B being Element of S st
( B = dom g & g is_measurable_on B ) & 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_measurable_on A ) & ex B being Element of S st
( B = dom g & g is_measurable_on B ) & 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_measurable_on A ) & ex B being Element of S st
( B = dom g & g is_measurable_on B ) & 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_measurable_on A ) & ex B being Element of S st
( B = dom g & g is_measurable_on B ) & 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_measurable_on A ) and
A2: ex B being Element of S st
( B = dom g & g is_measurable_on B ) 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 without-infty by A4, Th18, Th21;
A6: g | ((dom f) /\ (dom g)) is nonnegative by A4, Th21;
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_measurable_on B by A2;
consider A being Element of S such that
A10: A = dom f and
A11: f is_measurable_on A 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, Th22;
A13: C = (dom g) /\ C by A8, XBOOLE_1:17, XBOOLE_1:28;
g is_measurable_on C by A9, MESFUNC1:30, XBOOLE_1:17;
then A14: g | C is_measurable_on C by A13, Th48;
A15: C = (dom f) /\ C by A10, XBOOLE_1:17, XBOOLE_1:28;
f is_measurable_on C by A11, MESFUNC1:30, XBOOLE_1:17;
then A16: f | C is_measurable_on C by A15, Th48;
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 without-infty by A3, Th18, Th21;
then A19: dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) = C /\ C by A10, A8, A17, A7, A5, Th22;
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, Th22;
A21: for x being set 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 set ; :: 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, Th21;
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