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_measurable_on E by A1, Def17;
set AB = E /\ (A \/ B);
A5: max+ (f | A) = (max+ f) | A by Th34;
A6: dom f = dom (max- f) by MESFUNC2:def 3;
then (max- f) | (A \/ B) = ((max- f) | E) | (A \/ B) by A3, GRFUNC_1:64;
then A7: (max- f) | (A \/ B) = (max- f) | (E /\ (A \/ B)) by RELAT_1:100;
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, Th87, MESFUNC2:28;
A9: f | A is_integrable_on M by A1, Th103;
then A10: 0 <= integral+ M,(max+ (f | A)) by Th102;
A11: f | B is_integrable_on M by A1, Th103;
then A12: 0 <= integral+ M,(max+ (f | B)) by Th102;
A13: 0 <= integral+ M,(max- (f | B)) by A11, Th102;
integral+ M,(max- (f | B)) < +infty by A11, Def17;
then reconsider g2 = integral+ M,(max- (f | B)) as Real by A13, XXREAL_0:14;
integral+ M,(max+ (f | B)) < +infty by A11, Def17;
then reconsider g1 = integral+ M,(max+ (f | B)) as Real by A12, XXREAL_0:14;
A14: (integral+ M,(max+ (f | B))) - (integral+ M,(max- (f | B))) = g1 - g2 by SUPINF_2:5;
A15: max- (f | A) = (max- f) | A by Th34;
A16: dom f = dom (max+ f) by MESFUNC2:def 2;
then (max+ f) | (A \/ B) = ((max+ f) | E) | (A \/ B) by A3, GRFUNC_1:64;
then A17: (max+ f) | (A \/ B) = (max+ f) | (E /\ (A \/ B)) by RELAT_1:100;
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, Th87, MESFUNC2:27;
A19: max- (f | B) = (max- f) | B by Th34;
A20: max+ (f | B) = (max+ f) | B by Th34;
integral+ M,(max+ (f | A)) < +infty by A9, Def17;
then reconsider f1 = integral+ M,(max+ (f | A)) as 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, Th102;
integral+ M,(max- (f | A)) < +infty by A9, Def17;
then reconsider f2 = integral+ M,(max- (f | A)) as 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:64
.= Integral M,(f | (E /\ (A \/ B))) by RELAT_1:100
.= (integral+ M,((max+ f) | (E /\ (A \/ B)))) - (integral+ M,(max- (f | (E /\ (A \/ B))))) by Th34
.= (integral+ M,((max+ f) | (E /\ (A \/ B)))) - (integral+ M,((max- f) | (E /\ (A \/ B)))) by Th34 ;
then Integral M,(f | (A \/ B)) = (f1 + g1) - (f2 + g2) by A18, A8, A17, A7, A5, A15, A20, A19, A21, A23, SUPINF_2:5;
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:5;
hence Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B)) by A24, A14, SUPINF_2:1; :: thesis: verum