theorem Th53: :: LPSPACE2:53

for X being non empty set
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) ) ) )