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_{3} -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_{2} -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_{1} -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

for M being sigma_Measure of S

for E being Element of S

for f being b

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

f is_integrable_on M

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being b

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