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 & 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)) )
consider A being Element of S such that
A4: ( A = dom f & f is_measurable_on A ) by A1;
consider B being Element of S such that
A5: ( B = dom g & g is_measurable_on B ) by A2;
set f1 = f | ((dom f) /\ (dom g));
set g1 = g | ((dom f) /\ (dom g));
take C = A /\ B; :: thesis: ( C = dom (f + g) & integral+ M,(f + g) = (integral+ M,(f | C)) + (integral+ M,(g | C)) )
A6: C = dom (f + g) by A4, A5, Th22, A3;
( dom (f | ((dom f) /\ (dom g))) = (dom f) /\ ((dom f) /\ (dom g)) & dom (g | ((dom f) /\ (dom g))) = (dom g) /\ ((dom f) /\ (dom g)) ) by RELAT_1:90;
then A7: ( dom (f | ((dom f) /\ (dom g))) = ((dom f) /\ (dom f)) /\ (dom g) & dom (g | ((dom f) /\ (dom g))) = ((dom g) /\ (dom g)) /\ (dom f) ) by XBOOLE_1:16;
( C c= dom f & C c= dom g ) by A4, A5, XBOOLE_1:17;
then ( f is_measurable_on C & C = (dom f) /\ C & g is_measurable_on C & C = (dom g) /\ C ) by A4, A5, MESFUNC1:34, XBOOLE_1:28;
then A8: ( f | C is_measurable_on C & g | C is_measurable_on C ) by Th48;
( f | ((dom f) /\ (dom g)) is nonnegative & g | ((dom f) /\ (dom g)) is nonnegative ) by A3, Th21;
then A9: 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 A4, A5, A7, A8, Lm11;
( f | ((dom f) /\ (dom g)) is without-infty & g | ((dom f) /\ (dom g)) is without-infty ) by A3, Th18, Th21;
then A10: ( dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) = (dom (f | ((dom f) /\ (dom g)))) /\ (dom (g | ((dom f) /\ (dom g)))) & dom ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) = C /\ C ) by A4, A5, A7, Th22;
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 A11: 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 A12: ( x in dom (f | ((dom f) /\ (dom g))) & x in dom (g | ((dom f) /\ (dom g))) ) by A10, 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 A11, MESFUNC1:def 3
.= (f . x) + ((g | ((dom f) /\ (dom g))) . x) by A12, FUNCT_1:70
.= (f . x) + (g . x) by A12, FUNCT_1:70 ;
hence ((f | ((dom f) /\ (dom g))) + (g | ((dom f) /\ (dom g)))) . x = (f + g) . x by A6, A10, A11, MESFUNC1:def 3; :: thesis: verum

end;

hence ( C = dom (f + g) & integral+ M,(f + g) = (integral+ M,(f | C)) + (integral+ M,(g | C)) ) by A4, A5, A6, A9, A10, FUNCT_1:9; :: thesis: verum