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 A1: ( f is_integrable_on M & A misses B ) ; :: thesis: Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B))
then consider E being Element of S such that
A2: ( E = dom f & f is_measurable_on E ) by Def17;
set AB = E /\ (A \/ B);
A3: ( integral+ M,(max+ (f | A)) <= integral+ M,(max+ f) & integral+ M,(max- (f | A)) <= integral+ M,(max- f) & f | A is_integrable_on M & integral+ M,(max+ (f | B)) <= integral+ M,(max+ f) & integral+ M,(max- (f | B)) <= integral+ M,(max- f) & f | B is_integrable_on M ) by A1, Th103;
then A4: ( ex C being Element of S st
( C = dom (f | A) & f | A is_measurable_on C ) & integral+ M,(max+ (f | A)) < +infty & integral+ M,(max- (f | A)) < +infty & ex C being Element of S st
( C = dom (f | B) & f | B is_measurable_on C ) & integral+ M,(max+ (f | B)) < +infty & integral+ M,(max- (f | B)) < +infty ) by Def17;
A5: ( 0 <= integral+ M,(max+ (f | A)) & 0 <= integral+ M,(max- (f | A)) & 0 <= integral+ M,(max+ (f | B)) & 0 <= integral+ M,(max- (f | B)) ) by A3, Th102;
A6: Integral M,(f | (A \/ B)) = Integral M,((f | E) | (A \/ B)) by A2, 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 ;
A7: ( dom f = dom (max+ f) & dom f = dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A8: ( max+ f is nonnegative & max- f is nonnegative ) by Lm1;
( max+ f is_measurable_on E & max- f is_measurable_on E ) by A2, MESFUNC2:27, MESFUNC2:28;
then A9: ( integral+ M,((max+ f) | (A \/ B)) = (integral+ M,((max+ f) | A)) + (integral+ M,((max+ f) | B)) & integral+ M,((max- f) | (A \/ B)) = (integral+ M,((max- f) | A)) + (integral+ M,((max- f) | B)) ) by A1, A2, A7, A8, Th87;
( (max+ f) | (A \/ B) = ((max+ f) | E) | (A \/ B) & (max- f) | (A \/ B) = ((max- f) | E) | (A \/ B) ) by A2, A7, GRFUNC_1:64;
then A10: ( (max+ f) | (A \/ B) = (max+ f) | (E /\ (A \/ B)) & (max- f) | (A \/ B) = (max- f) | (E /\ (A \/ B)) ) by RELAT_1:100;
A11: ( max+ (f | A) = (max+ f) | A & max- (f | A) = (max- f) | A & max+ (f | B) = (max+ f) | B & max- (f | B) = (max- f) | B ) by Th34;
reconsider f1 = integral+ M,(max+ (f | A)) as Real by A4, A5, XXREAL_0:14;
reconsider f2 = integral+ M,(max- (f | A)) as Real by A4, A5, XXREAL_0:14;
reconsider g1 = integral+ M,(max+ (f | B)) as Real by A4, A5, XXREAL_0:14;
reconsider g2 = integral+ M,(max- (f | B)) as Real by A4, A5, XXREAL_0:14;
( (integral+ M,(max+ (f | A))) + (integral+ M,(max+ (f | B))) = f1 + g1 & (integral+ M,(max- (f | A))) + (integral+ M,(max- (f | B))) = f2 + g2 ) by SUPINF_2:1;
then Integral M,(f | (A \/ B)) = (f1 + g1) - (f2 + g2) by A6, A9, A10, A11, SUPINF_2:5;
then A12: Integral M,(f | (A \/ B)) = (f1 - f2) + (g1 - g2) ;
( (integral+ M,(max+ (f | A))) - (integral+ M,(max- (f | A))) = f1 - f2 & (integral+ M,(max+ (f | B))) - (integral+ M,(max- (f | B))) = g1 - g2 ) by SUPINF_2:5;
hence Integral M,(f | (A \/ B)) = (Integral M,(f | A)) + (Integral M,(f | B)) by A12, SUPINF_2:1; :: thesis: verum