let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being b₃ -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds
f is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for f being b₂ -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds
f is_integrable_on M
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being b₁ -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds
f is_integrable_on M
let E be Element of S; :: thesis: for f being E -measurable PartFunc of X,ExtREAL st dom f c= E & f is_a.e.integrable_on M holds
f is_integrable_on M
let f be E -measurable PartFunc of X,ExtREAL; :: thesis: ( dom f c= E & f is_a.e.integrable_on M implies f is_integrable_on M )
assume that
A1: dom f c= E and
A2: f is_a.e.integrable_on M ; :: thesis: f is_integrable_on M
reconsider E1 = dom f as Element of S by A2, Th16;
consider A being Element of S such that
A3: ( M . A = 0 & A c= dom f & f | (A `) is_integrable_on M ) by A2;
A4: f | (A `) = f | ((dom f) \ A) by Th15;
then A5: dom (f | (A `)) = (dom f) /\ ((dom f) \ A) by RELAT_1:61;
then A6: dom (f | (A `)) = (E1 /\ E1) \ A by XBOOLE_1:49
.= E1 \ A ;
then A7: ( dom (max+ (f | (A `))) = E1 \ A & dom (max- (f | (A `))) = E1 \ A ) by MESFUNC2:def 2, MESFUNC2:def 3;
A8: f is E1 -measurable by A1, MESFUNC1:30;
then f is E1 \ A -measurable by XBOOLE_1:36, MESFUNC1:30;
then f | (A `) is E1 \ A -measurable by A4, A5, A6, MESFUNC5:42;
then A9: ( max+ (f | (A `)) is E1 \ A -measurable & max- (f | (A `)) is E1 \ A -measurable ) by A6, MESFUNC2:25, MESFUNC2:26;
A10: ( E1 = dom (max+ f) & E1 = dom (max- f) ) by MESFUNC2:def 2, MESFUNC2:def 3;
A11: ( max+ f is nonnegative & max- f is nonnegative ) by MESFUN11:5;
( Integral (M,((max+ f) | ((dom f) \ A))) = Integral (M,(max+ f)) & Integral (M,((max- f) | ((dom f) \ A))) = Integral (M,(max- f)) ) by A3, A8, A10, MESFUNC2:25, MESFUNC2:26, MESFUNC5:95;
then ( Integral (M,(max+ (f | (A `)))) = Integral (M,(max+ f)) & Integral (M,(max- (f | (A `)))) = Integral (M,(max- f)) ) by A4, MESFUNC5:28;
then ( integral+ (M,(max+ (f | (A `)))) = Integral (M,(max+ f)) & integral+ (M,(max- (f | (A `)))) = Integral (M,(max- f)) ) by A7, A9, MESFUNC5:88, MESFUN11:5;
then A12: ( integral+ (M,(max+ (f | (A `)))) = integral+ (M,(max+ f)) & integral+ (M,(max- (f | (A `)))) = integral+ (M,(max- f)) ) by A8, A10, A11, MESFUNC2:25, MESFUNC2:26, MESFUNC5:88;
( integral+ (M,(max+ (f | (A `)))) < +infty & integral+ (M,(max- (f | (A `)))) < +infty ) by A3, MESFUNC5:def 17;
hence f is_integrable_on M by A8, A12, MESFUNC5:def 17; :: thesis: verum