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 being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & A misses B holds

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

let A, B be Element of S; :: thesis: ( f is_integrable_on M & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

assume that

A1: f is_integrable_on M and

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

consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable by A1;

set AB = E /\ (A \/ B);

A5: max+ (f | A) = (max+ f) | A by Th28;

A6: dom f = dom (max- f) by MESFUNC2:def 3;

then (max- f) | (A \/ B) = ((max- f) | E) | (A \/ B) by A3, GRFUNC_1:23;

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

max- f is nonnegative by Lm1;

then A8: integral+ (M,((max- f) | (A \/ B))) = (integral+ (M,((max- f) | A))) + (integral+ (M,((max- f) | B))) by A2, A3, A4, A6, Th81, MESFUNC2:26;

A9: f | A is_integrable_on M by A1, Th97;

then A10: 0 <= integral+ (M,(max+ (f | A))) by Th96;

A11: f | B is_integrable_on M by A1, Th97;

then A12: 0 <= integral+ (M,(max+ (f | B))) by Th96;

A13: 0 <= integral+ (M,(max- (f | B))) by A11, Th96;

integral+ (M,(max- (f | B))) < +infty by A11;

then reconsider g2 = integral+ (M,(max- (f | B))) as Element of REAL by A13, XXREAL_0:14;

integral+ (M,(max+ (f | B))) < +infty by A11;

then reconsider g1 = integral+ (M,(max+ (f | B))) as Element of REAL by A12, XXREAL_0:14;

A14: (integral+ (M,(max+ (f | B)))) - (integral+ (M,(max- (f | B)))) = g1 - g2 by SUPINF_2:3;

A15: max- (f | A) = (max- f) | A by Th28;

A16: dom f = dom (max+ f) by MESFUNC2:def 2;

then (max+ f) | (A \/ B) = ((max+ f) | E) | (A \/ B) by A3, GRFUNC_1:23;

then A17: (max+ f) | (A \/ B) = (max+ f) | (E /\ (A \/ B)) by RELAT_1:71;

max+ f is nonnegative by Lm1;

then A18: integral+ (M,((max+ f) | (A \/ B))) = (integral+ (M,((max+ f) | A))) + (integral+ (M,((max+ f) | B))) by A2, A3, A4, A16, Th81, MESFUNC2:25;

A19: max- (f | B) = (max- f) | B by Th28;

A20: max+ (f | B) = (max+ f) | B by Th28;

integral+ (M,(max+ (f | A))) < +infty by A9;

then reconsider f1 = integral+ (M,(max+ (f | A))) as Element of REAL by A10, XXREAL_0:14;

A21: (integral+ (M,(max+ (f | A)))) + (integral+ (M,(max+ (f | B)))) = f1 + g1 by SUPINF_2:1;

A22: 0 <= integral+ (M,(max- (f | A))) by A9, Th96;

integral+ (M,(max- (f | A))) < +infty by A9;

then reconsider f2 = integral+ (M,(max- (f | A))) as Element of REAL by A22, XXREAL_0:14;

A23: (integral+ (M,(max- (f | A)))) + (integral+ (M,(max- (f | B)))) = f2 + g2 by SUPINF_2:1;

Integral (M,(f | (A \/ B))) = Integral (M,((f | E) | (A \/ B))) by A3, GRFUNC_1:23

.= Integral (M,(f | (E /\ (A \/ B)))) by RELAT_1:71

.= (integral+ (M,((max+ f) | (E /\ (A \/ B))))) - (integral+ (M,(max- (f | (E /\ (A \/ B)))))) by Th28

.= (integral+ (M,((max+ f) | (E /\ (A \/ B))))) - (integral+ (M,((max- f) | (E /\ (A \/ B))))) by Th28 ;

then Integral (M,(f | (A \/ B))) = (f1 + g1) - (f2 + g2) by A18, A8, A17, A7, A5, A15, A20, A19, A21, A23, SUPINF_2:3;

then A24: Integral (M,(f | (A \/ B))) = (f1 - f2) + (g1 - g2) ;

(integral+ (M,(max+ (f | A)))) - (integral+ (M,(max- (f | A)))) = f1 - f2 by SUPINF_2:3;

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A24, A14, SUPINF_2:1; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A, B being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & 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 being Element of S st f is_integrable_on M & A misses B holds

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

let A, B be Element of S; :: thesis: ( f is_integrable_on M & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )

assume that

A1: f is_integrable_on M and

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

consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable by A1;

set AB = E /\ (A \/ B);

A5: max+ (f | A) = (max+ f) | A by Th28;

A6: dom f = dom (max- f) by MESFUNC2:def 3;

then (max- f) | (A \/ B) = ((max- f) | E) | (A \/ B) by A3, GRFUNC_1:23;

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

max- f is nonnegative by Lm1;

then A8: integral+ (M,((max- f) | (A \/ B))) = (integral+ (M,((max- f) | A))) + (integral+ (M,((max- f) | B))) by A2, A3, A4, A6, Th81, MESFUNC2:26;

A9: f | A is_integrable_on M by A1, Th97;

then A10: 0 <= integral+ (M,(max+ (f | A))) by Th96;

A11: f | B is_integrable_on M by A1, Th97;

then A12: 0 <= integral+ (M,(max+ (f | B))) by Th96;

A13: 0 <= integral+ (M,(max- (f | B))) by A11, Th96;

integral+ (M,(max- (f | B))) < +infty by A11;

then reconsider g2 = integral+ (M,(max- (f | B))) as Element of REAL by A13, XXREAL_0:14;

integral+ (M,(max+ (f | B))) < +infty by A11;

then reconsider g1 = integral+ (M,(max+ (f | B))) as Element of REAL by A12, XXREAL_0:14;

A14: (integral+ (M,(max+ (f | B)))) - (integral+ (M,(max- (f | B)))) = g1 - g2 by SUPINF_2:3;

A15: max- (f | A) = (max- f) | A by Th28;

A16: dom f = dom (max+ f) by MESFUNC2:def 2;

then (max+ f) | (A \/ B) = ((max+ f) | E) | (A \/ B) by A3, GRFUNC_1:23;

then A17: (max+ f) | (A \/ B) = (max+ f) | (E /\ (A \/ B)) by RELAT_1:71;

max+ f is nonnegative by Lm1;

then A18: integral+ (M,((max+ f) | (A \/ B))) = (integral+ (M,((max+ f) | A))) + (integral+ (M,((max+ f) | B))) by A2, A3, A4, A16, Th81, MESFUNC2:25;

A19: max- (f | B) = (max- f) | B by Th28;

A20: max+ (f | B) = (max+ f) | B by Th28;

integral+ (M,(max+ (f | A))) < +infty by A9;

then reconsider f1 = integral+ (M,(max+ (f | A))) as Element of REAL by A10, XXREAL_0:14;

A21: (integral+ (M,(max+ (f | A)))) + (integral+ (M,(max+ (f | B)))) = f1 + g1 by SUPINF_2:1;

A22: 0 <= integral+ (M,(max- (f | A))) by A9, Th96;

integral+ (M,(max- (f | A))) < +infty by A9;

then reconsider f2 = integral+ (M,(max- (f | A))) as Element of REAL by A22, XXREAL_0:14;

A23: (integral+ (M,(max- (f | A)))) + (integral+ (M,(max- (f | B)))) = f2 + g2 by SUPINF_2:1;

Integral (M,(f | (A \/ B))) = Integral (M,((f | E) | (A \/ B))) by A3, GRFUNC_1:23

.= Integral (M,(f | (E /\ (A \/ B)))) by RELAT_1:71

.= (integral+ (M,((max+ f) | (E /\ (A \/ B))))) - (integral+ (M,(max- (f | (E /\ (A \/ B)))))) by Th28

.= (integral+ (M,((max+ f) | (E /\ (A \/ B))))) - (integral+ (M,((max- f) | (E /\ (A \/ B))))) by Th28 ;

then Integral (M,(f | (A \/ B))) = (f1 + g1) - (f2 + g2) by A18, A8, A17, A7, A5, A15, A20, A19, A21, A23, SUPINF_2:3;

then A24: Integral (M,(f | (A \/ B))) = (f1 - f2) + (g1 - g2) ;

(integral+ (M,(max+ (f | A)))) - (integral+ (M,(max- (f | A)))) = f1 - f2 by SUPINF_2:3;

hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A24, A14, SUPINF_2:1; :: thesis: verum