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 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,ExtREAL
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,ExtREAL
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,ExtREAL; :: 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 & B c= dom f ) and
A2: f | A is_integrable_on M and
A3: f | B is_integrable_on M ; :: thesis: f | (A \/ B) is_integrable_on M
set f1 = f | (A \/ B);
A4: ( A = dom (f | A) & B = dom (f | B) ) by A1, RELAT_1:62;
A5: ex E being Element of S st
( E = dom (f | A) & f | A is E -measurable ) by A2, MESFUNC5:def 17;
then reconsider A1 = A as Element of S by A1, RELAT_1:62;
A6: ex E being Element of S st
( E = dom (f | B) & f | B is E -measurable ) by A3, MESFUNC5:def 17;
then reconsider B1 = B as Element of S by A1, RELAT_1:62;
A7: ( integral+ (M,(max+ (f | A))) < +infty & integral+ (M,(max- (f | A))) < +infty ) by A2, MESFUNC5:def 17;
A8: ( integral+ (M,(max+ (f | B))) < +infty & integral+ (M,(max- (f | B))) < +infty ) by A3, MESFUNC5:def 17;
A9: dom (f | (A \/ B)) = (dom f) /\ (A \/ B) by RELAT_1:61
.= ((dom f) /\ A) \/ ((dom f) /\ B) by XBOOLE_1:23 ;
A10: ( dom (f | A) = (dom f) /\ A & dom (f | B) = (dom f) /\ B ) by RELAT_1:61;
A11: ( (f | (A \/ B)) | A = f | A & (f | (A \/ B)) | B = f | B ) by XBOOLE_1:7, RELAT_1:74;
then ( f | (A \/ B) is A1 -measurable & f | (A \/ B) is B1 -measurable ) by A4, A5, A6, MESFUN13:19;
then A12: f | (A \/ B) is A1 \/ B1 -measurable by MESFUNC1:31;
A13: ( dom (max+ (f | (A \/ B))) = dom (f | (A \/ B)) & dom (max- (f | (A \/ B))) = dom (f | (A \/ B)) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A14: ( max+ (f | (A \/ B)) is nonnegative & max- (f | (A \/ B)) is nonnegative ) by MESFUN11:5;
A15: ( (max+ (f | (A \/ B))) | A = max+ (f | A) & (max+ (f | (A \/ B))) | B = max+ (f | B) & (max- (f | (A \/ B))) | A = max- (f | A) & (max- (f | (A \/ B))) | B = max- (f | B) ) by A11, MESFUNC5:28;
A16: (max+ (f | (A \/ B))) | (A \/ B) = max+ ((f | (A \/ B)) | (A \/ B)) by MESFUNC5:28
.= max+ (f | (A \/ B)) ;
A17: (max- (f | (A \/ B))) | (A \/ B) = max- ((f | (A \/ B)) | (A \/ B)) by MESFUNC5:28
.= max- (f | (A \/ B)) ;
A18: integral+ (M,((max+ (f | (A \/ B))) | (A \/ B))) <= (integral+ (M,((max+ (f | (A \/ B))) | A))) + (integral+ (M,((max+ (f | (A \/ B))) | B))) by A13, A4, A9, A10, A14, Th51, A12, MESFUNC2:25;
(integral+ (M,((max+ (f | (A \/ B))) | A))) + (integral+ (M,((max+ (f | (A \/ B))) | B))) <> +infty by A7, A8, A15, XXREAL_3:16;
then A19: integral+ (M,(max+ (f | (A \/ B)))) < +infty by A16, A18, XXREAL_0:2, XXREAL_0:4;
A20: integral+ (M,((max- (f | (A \/ B))) | (A \/ B))) <= (integral+ (M,((max- (f | (A \/ B))) | A))) + (integral+ (M,((max- (f | (A \/ B))) | B))) by A13, A4, A9, A10, A14, Th51, A12, MESFUNC2:26;
(integral+ (M,((max- (f | (A \/ B))) | A))) + (integral+ (M,((max- (f | (A \/ B))) | B))) <> +infty by A7, A8, A15, XXREAL_3:16;
then integral+ (M,(max- (f | (A \/ B)))) < +infty by A17, A20, XXREAL_0:2, XXREAL_0:4;
hence f | (A \/ B) is_integrable_on M by A4, A9, A10, A12, A19, MESFUNC5:def 17; :: thesis: verum