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 VSPDef6X;
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 DefLpNORM;

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 K1: 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 K2: g in Lp_Functions M,k by Lm10;
Integral M,((abs g) to_power k) = Integral M,((abs f) to_power k) by A1, Lm17, K1;
hence ex r being Real st
( 0 <= r & r = Integral M,((abs g) to_power k) & ||.x.|| = r to_power (1 / k) ) by A1, K2, Lm15; :: thesis: verum

end;