let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for k being positive Real st ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) & g in a.e-eq-class_Lp (f,M,k) holds
( g a.e.= f,M & f in Lp_Functions (M,k) )

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

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

let f, g be PartFunc of X,REAL; :: thesis: for k being positive Real st ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) & g in a.e-eq-class_Lp (f,M,k) holds
( g a.e.= f,M & f in Lp_Functions (M,k) )

let k be positive Real; :: thesis: ( ex E being Element of S st
( M . (E `) = 0 & E = dom f & f is E -measurable ) & g in a.e-eq-class_Lp (f,M,k) implies ( g a.e.= f,M & f in Lp_Functions (M,k) ) )

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