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 st ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) holds
a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) holds
a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) holds
a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)

let f be PartFunc of X,REAL; :: thesis: ( ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) implies a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M) )

assume A1: ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) ; :: thesis: a.e-eq-class_Lp (f,M,1) c= a.e-eq-class (f,M)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a.e-eq-class_Lp (f,M,1) or x in a.e-eq-class (f,M) )
assume x in a.e-eq-class_Lp (f,M,1) ; :: thesis: x in a.e-eq-class (f,M)
then consider h being PartFunc of X,REAL such that
A2: ( x = h & h in Lp_Functions (M,1) & f a.e.= h,M ) ;
A3: ex g being PartFunc of X,REAL st
( h = g & ex E being Element of S st
( M . (E `) = 0 & dom g = E & g is E -measurable & (abs g) to_power 1 is_integrable_on M ) ) by A2;
then consider Eh being Element of S such that
A4: ( M . (Eh `) = 0 & dom h = Eh & h is Eh -measurable & (abs h) to_power 1 is_integrable_on M ) ;
A5: dom ((abs h) to_power 1) = dom (abs h) by MESFUN6C:def 4;
for x being Element of X st x in dom ((abs h) to_power 1) holds
((abs h) to_power 1) . x = (abs h) . x
proof
let x be Element of X; :: thesis: ( x in dom ((abs h) to_power 1) implies ((abs h) to_power 1) . x = (abs h) . x )
assume x in dom ((abs h) to_power 1) ; :: thesis: ((abs h) to_power 1) . x = (abs h) . x
then ((abs h) to_power 1) . x = ((abs h) . x) to_power 1 by MESFUN6C:def 4;
hence ((abs h) to_power 1) . x = (abs h) . x by POWER:25; :: thesis: verum
end;
then (abs h) to_power 1 = abs h by ;
then A6: h is_integrable_on M by ;
reconsider ND = Eh ` as Element of S by MEASURE1:34;
( M . ND = 0 & dom h = ND ` ) by A4;
then A7: h in L1_Functions M by A6;
ex E being Element of S st
( M . E = 0 & dom f = E ` & f is_integrable_on M )
proof
consider Ef being Element of S such that
A8: ( M . (Ef `) = 0 & Ef = dom f & f is Ef -measurable ) by A1;
reconsider E = Ef ` as Element of S by MEASURE1:34;
take E ; :: thesis: ( M . E = 0 & dom f = E ` & f is_integrable_on M )
consider EE being Element of S such that
A9: ( M . EE = 0 & f | (EE `) = h | (EE `) ) by A2;
reconsider E1 = ND \/ EE as Element of S ;
( ND is measure_zero of M & EE is measure_zero of M ) by ;
then E1 is measure_zero of M by MEASURE1:37;
then A10: M . E1 = 0 by MEASURE1:def 7;
EE c= E1 by XBOOLE_1:7;
then E1 ` c= EE ` by SUBSET_1:12;
then A11: ( f | (E1 `) = (f | (EE `)) | (E1 `) & h | (E1 `) = (h | (EE `)) | (E1 `) ) by FUNCT_1:51;
A12: ( dom (max+ ()) = Ef & dom (max- ()) = Ef ) by ;
A13: ( Ef = dom () & R_EAL f is Ef -measurable ) by A8;
then A14: ( max+ () is Ef -measurable & max- () is Ef -measurable ) by ;
( ( for x being Element of X holds 0. <= (max+ ()) . x ) & ( for x being Element of X holds 0. <= (max- ()) . x ) ) by ;
then A15: ( max+ () is nonnegative & max- () is nonnegative ) by SUPINF_2:39;
A16: Ef = (Ef /\ E1) \/ (Ef \ E1) by XBOOLE_1:51;
reconsider E0 = Ef /\ E1 as Element of S ;
A17: Ef \ E1 = Ef /\ (E1 `) by SUBSET_1:13;
reconsider E2 = Ef \ E1 as Element of S ;
( max+ () = (max+ ()) | (dom (max+ ())) & max- () = (max- ()) | (dom (max- ())) ) by RELAT_1:69;
then A18: ( integral+ (M,(max+ ())) = (integral+ (M,((max+ ()) | E0))) + (integral+ (M,((max+ ()) | E2))) & integral+ (M,(max- ())) = (integral+ (M,((max- ()) | E0))) + (integral+ (M,((max- ()) | E2))) ) by ;
A19: ( integral+ (M,((max+ ()) | E0)) >= 0 & integral+ (M,((max- ()) | E0)) >= 0 ) by ;
( integral+ (M,((max+ ()) | E1)) = 0 & integral+ (M,((max- ()) | E1)) = 0 ) by ;
then ( integral+ (M,((max+ ()) | E0)) = 0 & integral+ (M,((max- ()) | E0)) = 0 ) by ;
then A20: ( integral+ (M,(max+ ())) = integral+ (M,((max+ ()) | E2)) & integral+ (M,(max- ())) = integral+ (M,((max- ()) | E2)) ) by ;
A21: E2 c= E1 ` by ;
then f | E2 = (h | (E1 `)) | E2 by ;
then A22: (R_EAL f) | E2 = () | E2 by ;
A23: ( (max+ ()) | E2 = max+ (() | E2) & (max+ ()) | E2 = max+ (() | E2) & (max- ()) | E2 = max- (() | E2) & (max- ()) | E2 = max- (() | E2) ) by MESFUNC5:28;
A24: R_EAL h is_integrable_on M by A6;
then A25: ( integral+ (M,(max+ ())) < +infty & integral+ (M,(max- ())) < +infty ) ;
( integral+ (M,(max+ (() | E2))) <= integral+ (M,(max+ ())) & integral+ (M,(max- (() | E2))) <= integral+ (M,(max- ())) ) by ;
then ( integral+ (M,(max+ ())) < +infty & integral+ (M,(max- ())) < +infty ) by ;
then R_EAL f is_integrable_on M by A13;
hence ( M . E = 0 & dom f = E ` & f is_integrable_on M ) by A8; :: thesis: verum
end;
then f in L1_Functions M ;
hence x in a.e-eq-class (f,M) by A2, A7; :: thesis: verum