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 )

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

hence
f in Lp_Functions (M,k)
; :: thesis: verum
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 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: verum

end;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 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: verum