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

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

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

f | ((dom f) /\ (dom g)) is nonnegative
by A3, Th15;
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;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

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