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

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,REAL

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let f be PartFunc of X,REAL; :: thesis: for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let k be positive Real; :: thesis: for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let x be Point of (Pre-Lp-Space (M,k)); :: thesis: ( f in x implies ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) )

assume A1: f in x ; :: thesis: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

x in the carrier of (Pre-Lp-Space (M,k)) ;

then x in CosetSet (M,k) by Def11;

then consider h being PartFunc of X,REAL such that

A2: ( x = a.e-eq-class_Lp (h,M,k) & h in Lp_Functions (M,k) ) ;

ex g being PartFunc of X,REAL st

( f = g & g in Lp_Functions (M,k) & h a.e.= g,M ) by A1, A2;

then ex f0 being PartFunc of X,REAL st

( f = f0 & ex ND being Element of S st

( M . (ND `) = 0 & dom f0 = ND & f0 is ND -measurable & (abs f0) to_power k is_integrable_on M ) ) ;

hence ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) ; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,REAL

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,REAL

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL

for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let f be PartFunc of X,REAL; :: thesis: for k being positive Real

for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let k be positive Real; :: thesis: for x being Point of (Pre-Lp-Space (M,k)) st f in x holds

( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

let x be Point of (Pre-Lp-Space (M,k)); :: thesis: ( f in x implies ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) )

assume A1: f in x ; :: thesis: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) )

x in the carrier of (Pre-Lp-Space (M,k)) ;

then x in CosetSet (M,k) by Def11;

then consider h being PartFunc of X,REAL such that

A2: ( x = a.e-eq-class_Lp (h,M,k) & h in Lp_Functions (M,k) ) ;

ex g being PartFunc of X,REAL st

( f = g & g in Lp_Functions (M,k) & h a.e.= g,M ) by A1, A2;

then ex f0 being PartFunc of X,REAL st

( f = f0 & ex ND being Element of S st

( M . (ND `) = 0 & dom f0 = ND & f0 is ND -measurable & (abs f0) to_power k is_integrable_on M ) ) ;

hence ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) ; :: thesis: verum