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 A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) 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 A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) 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 A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) 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 A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B be Element of S; :: thesis: ( A \/ B c= dom f & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1: A \/ B c= dom f and
A2: f is A \/ B -measurable and
A3: A misses B and
A4: ( integral+ (M,(max+ (f | (A \/ B)))) < +infty or integral+ (M,(max- (f | (A \/ B)))) < +infty ) ; :: thesis: Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
set g = f | (A \/ B);
A5: dom (f | (A \/ B)) = A \/ B by A1, RELAT_1:62;
A \/ B = (dom f) /\ (A \/ B) by A1, XBOOLE_1:28;
then A6: f | (A \/ B) is A \/ B -measurable by A2, MESFUNC5:42;
( (f | (A \/ B)) | A = f | A & (f | (A \/ B)) | B = f | B ) by RELAT_1:74, XBOOLE_1:7;
hence Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A6, A5, A3, A4, Lm2; :: thesis: verum