let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let f be PartFunc of X,ExtREAL; :: thesis: for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let A, B, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

assume that

A1: ( E = dom f & f is E -measurable ) and

A2: f is nonpositive and

A3: A misses B ; :: thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

set f1 = f | (A \/ B);

set f2 = f | A;

set f3 = f | B;

set g = - f;

reconsider E1 = E /\ (A \/ B) as Element of S ;

A4: dom (f | (A \/ B)) = E1 by A1, RELAT_1:61;

A5: E1 = (dom f) /\ E1 by A1, XBOOLE_1:17, XBOOLE_1:28;

A6: f is E1 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A7: f | E1 = (f | E) | (A \/ B) by RELAT_1:71;

(- f) | (A \/ B) = - (f | (A \/ B)) by Th3;

then A8: Integral (M,((- f) | (A \/ B))) = - (Integral (M,(f | (A \/ B)))) by A1, A4, A5, A6, A7, Th52, MESFUNC5:42;

reconsider E2 = E /\ A as Element of S ;

A9: dom (f | A) = E2 by A1, RELAT_1:61;

A10: E2 = (dom f) /\ E2 by A1, XBOOLE_1:17, XBOOLE_1:28;

A11: f is E2 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A12: f | E2 = (f | E) | A by RELAT_1:71;

(- f) | A = - (f | A) by Th3;

then A13: Integral (M,((- f) | A)) = - (Integral (M,(f | A))) by A1, A9, A10, A11, A12, Th52, MESFUNC5:42;

reconsider E3 = E /\ B as Element of S ;

A14: dom (f | B) = E3 by A1, RELAT_1:61;

A15: E3 = (dom f) /\ E3 by A1, XBOOLE_1:17, XBOOLE_1:28;

A16: f is E3 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A17: f | E3 = (f | E) | B by RELAT_1:71;

(- f) | B = - (f | B) by Th3;

then A18: Integral (M,((- f) | B)) = - (Integral (M,(f | B))) by A1, A14, A15, A16, A17, Th52, MESFUNC5:42;

E = dom (- f) by A1, MESFUNC1:def 7;

then Integral (M,((- f) | (A \/ B))) = (Integral (M,((- f) | A))) + (Integral (M,((- f) | B))) by A2, A3, A1, MEASUR11:63, MESFUNC5:91;

then - (Integral (M,(f | (A \/ B)))) = - ((Integral (M,(f | A))) + (Integral (M,(f | B)))) by A8, A13, A18, XXREAL_3:9;

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by XXREAL_3:10; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let f be PartFunc of X,ExtREAL; :: thesis: for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds

Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

let A, B, E be Element of S; :: thesis: ( E = dom f & f is E -measurable & f is nonpositive & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

assume that

A1: ( E = dom f & f is E -measurable ) and

A2: f is nonpositive and

A3: A misses B ; :: thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

set f1 = f | (A \/ B);

set f2 = f | A;

set f3 = f | B;

set g = - f;

reconsider E1 = E /\ (A \/ B) as Element of S ;

A4: dom (f | (A \/ B)) = E1 by A1, RELAT_1:61;

A5: E1 = (dom f) /\ E1 by A1, XBOOLE_1:17, XBOOLE_1:28;

A6: f is E1 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A7: f | E1 = (f | E) | (A \/ B) by RELAT_1:71;

(- f) | (A \/ B) = - (f | (A \/ B)) by Th3;

then A8: Integral (M,((- f) | (A \/ B))) = - (Integral (M,(f | (A \/ B)))) by A1, A4, A5, A6, A7, Th52, MESFUNC5:42;

reconsider E2 = E /\ A as Element of S ;

A9: dom (f | A) = E2 by A1, RELAT_1:61;

A10: E2 = (dom f) /\ E2 by A1, XBOOLE_1:17, XBOOLE_1:28;

A11: f is E2 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A12: f | E2 = (f | E) | A by RELAT_1:71;

(- f) | A = - (f | A) by Th3;

then A13: Integral (M,((- f) | A)) = - (Integral (M,(f | A))) by A1, A9, A10, A11, A12, Th52, MESFUNC5:42;

reconsider E3 = E /\ B as Element of S ;

A14: dom (f | B) = E3 by A1, RELAT_1:61;

A15: E3 = (dom f) /\ E3 by A1, XBOOLE_1:17, XBOOLE_1:28;

A16: f is E3 -measurable by A1, XBOOLE_1:17, MESFUNC1:30;

A17: f | E3 = (f | E) | B by RELAT_1:71;

(- f) | B = - (f | B) by Th3;

then A18: Integral (M,((- f) | B)) = - (Integral (M,(f | B))) by A1, A14, A15, A16, A17, Th52, MESFUNC5:42;

E = dom (- f) by A1, MESFUNC1:def 7;

then Integral (M,((- f) | (A \/ B))) = (Integral (M,((- f) | A))) + (Integral (M,((- f) | B))) by A2, A3, A1, MEASUR11:63, MESFUNC5:91;

then - (Integral (M,(f | (A \/ B)))) = - ((Integral (M,(f | A))) + (Integral (M,(f | B)))) by A8, A13, A18, XXREAL_3:9;

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by XXREAL_3:10; :: thesis: verum