let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,REAL; :: thesis:
let k be positive Real; :: thesis:
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:
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:
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 )

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:
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 A6, VALUED_1:def 11;
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 MESFUNC2:def 2, MESFUNC2:def 3;
abs f is Ef -measurable by A6, MESFUNC6:48;
then (abs f) to_power k is Ef -measurable by A9, MESFUN6C:29;
then A11: ( Ef = dom (R_EAL ((abs f) to_power k)) & R_EAL ((abs f) to_power k) is Ef -measurable ) by A9, MESFUN6C:def 4;
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 MESFUNC2:25, MESFUNC2:26;
( ( 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 MESFUNC2:12, MESFUNC2:13;
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 A10, A12, A13, A14, MESFUNC5:81, XBOOLE_1:89;
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 A12, A13, A10, MESFUNC5:80;
( ND is measure_zero of M & EE is measure_zero of M ) by A5, A7, MEASURE1:def 7;
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 A10, A12, A13, MESFUNC5:82;
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 A10, A12, A13, A16, MESFUNC5:83, XBOOLE_1:17;
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 A15, XXREAL_3:4;
Ef \ E1 = Ef /\ (E1 `) by SUBSET_1:13;
then A18: E2 c= E1 ` by XBOOLE_1:17;
then f | E2 = (g | (E1 `)) | E2 by A7, A8, FUNCT_1:51;
then A19: f | E2 = g | E2 by A18, FUNCT_1:51;
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 A23, MESFUNC5:97;
then ( integral+ (M,(max+ (R_EAL ((abs f) to_power k)))) < +infty & integral+ (M,(max- (R_EAL ((abs f) to_power k)))) < +infty ) by A17, A19, A20, A21, A22, A24, XXREAL_0:2;
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:

end;

hence f in Lp_Functions (M,k) ; :: thesis: