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,REAL
for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL
for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL
for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M
let f be PartFunc of X,REAL; :: thesis: for A, B being set st A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M holds
f | (A \/ B) is_integrable_on M
let A, B be set ; :: thesis: ( A c= dom f & B c= dom f & f | A is_integrable_on M & f | B is_integrable_on M implies f | (A \/ B) is_integrable_on M )
assume that
A1: A c= dom f and
A2: B c= dom f and
A3: f | A is_integrable_on M and
A4: f | B is_integrable_on M ; :: thesis: f | (A \/ B) is_integrable_on M
A5: ( A c= dom (R_EAL f) & B c= dom (R_EAL f) ) by A1, A2, MESFUNC5:def 7;
( R_EAL (f | A) is_integrable_on M & R_EAL (f | B) is_integrable_on M ) by A3, A4, MESFUNC6:def 4;
then ( (R_EAL f) | A is_integrable_on M & (R_EAL f) | B is_integrable_on M ) by Th16;
then (R_EAL f) | (A \/ B) is_integrable_on M by A5, Th52;
then R_EAL (f | (A \/ B)) is_integrable_on M by Th16;
hence f | (A \/ B) is_integrable_on M by MESFUNC6:def 4; :: thesis: verum