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 ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative 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 ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative 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 ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative 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 ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative holds
integral+ (M,(f | (A \/ B))) <= (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
let A, B be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is E -measurable ) & f is nonnegative implies integral+ (M,(f | (A \/ B))) <= (integral+ (M,(f | A))) + (integral+ (M,(f | B))) )
assume that
A1: ex E being Element of S st
( E = dom f & f is E -measurable ) and
A2: f is nonnegative ; :: thesis: integral+ (M,(f | (A \/ B))) <= (integral+ (M,(f | A))) + (integral+ (M,(f | B)))
set A1 = A \ B;
A3: integral+ (M,(f | (A \ B))) <= integral+ (M,(f | A)) by A1, A2, XBOOLE_1:36, MESFUNC5:83;
A4: (A \ B) \/ B = A \/ B by XBOOLE_1:39;
integral+ (M,(f | ((A \ B) \/ B))) = (integral+ (M,(f | (A \ B)))) + (integral+ (M,(f | B))) by A1, A2, MESFUNC5:81, XBOOLE_1:79;
hence integral+ (M,(f | (A \/ B))) <= (integral+ (M,(f | A))) + (integral+ (M,(f | B))) by A3, A4, XXREAL_3:35; :: thesis: verum