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 b3 -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 b2 -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 b1 -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:
reconsider E1 = dom f as Element of S by ;
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 ;
A8: f is E1 -measurable by ;
then f is E1 \ A -measurable by ;
then f | (A `) is E1 \ A -measurable by ;
then A9: ( max+ (f | (A `)) is E1 \ A -measurable & max- (f | (A `)) is E1 \ A -measurable ) by ;
A10: ( E1 = dom (max+ f) & E1 = dom (max- f) ) by ;
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 ;
then ( Integral (M,(max+ (f | (A `)))) = Integral (M,(max+ f)) & Integral (M,(max- (f | (A `)))) = Integral (M,(max- f)) ) by ;
then ( integral+ (M,(max+ (f | (A `)))) = Integral (M,(max+ f)) & integral+ (M,(max- (f | (A `)))) = Integral (M,(max- f)) ) by ;
then A12: ( integral+ (M,(max+ (f | (A `)))) = integral+ (M,(max+ f)) & integral+ (M,(max- (f | (A `)))) = integral+ (M,(max- f)) ) by ;
( integral+ (M,(max+ (f | (A `)))) < +infty & integral+ (M,(max- (f | (A `)))) < +infty ) by ;
hence f is_integrable_on M by ; :: thesis: verum