let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

let M be sigma_Measure of S; :: thesis: for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

let x be Point of (Lp-Space (M,k)); :: thesis: ( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

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

then ex g being PartFunc of X,REAL st

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

hence ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) ; :: thesis: for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) )

consider f being PartFunc of X,REAL such that

A1: ( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & (Lp-Norm (M,k)) . x = r to_power (1 / k) ) ) by Def12;

for M being sigma_Measure of S

for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

let M be sigma_Measure of S; :: thesis: for k being positive Real

for x being Point of (Lp-Space (M,k)) holds

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

let x be Point of (Lp-Space (M,k)); :: thesis: ( ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) & ( for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) ) ) )

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

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

then ex g being PartFunc of X,REAL st

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

hence ex f being PartFunc of X,REAL st

( f in Lp_Functions (M,k) & x = a.e-eq-class_Lp (f,M,k) ) ; :: thesis: for f being PartFunc of X,REAL st f in x holds

ex r being Real st

( 0 <= r & r = Integral (M,((abs f) to_power k)) & ||.x.|| = r to_power (1 / k) )

consider f being PartFunc of X,REAL such that

A1: ( f in x & ex r being Real st

( r = Integral (M,((abs f) to_power k)) & (Lp-Norm (M,k)) . x = r to_power (1 / k) ) ) by Def12;

hereby :: thesis: verum

let g be PartFunc of X,REAL; :: thesis: ( g in x implies ex r being Real st

( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) ) )

assume A2: g in x ; :: thesis: ex r being Real st

( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) )

then A3: g in Lp_Functions (M,k) by Th50;

Integral (M,((abs g) to_power k)) = Integral (M,((abs f) to_power k)) by A1, Th52, A2;

hence ex r being Real st

( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) ) by A1, A3, Th49; :: thesis: verum

end;( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) ) )

assume A2: g in x ; :: thesis: ex r being Real st

( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) )

then A3: g in Lp_Functions (M,k) by Th50;

Integral (M,((abs g) to_power k)) = Integral (M,((abs f) to_power k)) by A1, Th52, A2;

hence ex r being Real st

( 0 <= r & r = Integral (M,((abs g) to_power k)) & ||.x.|| = r to_power (1 / k) ) by A1, A3, Th49; :: thesis: verum