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