for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for x being Point of (L-1-Space M) holds
( ex f being PartFunc of X,REAL st
( f in L1_Functions M & x = a.e-eq-class (f,M) & ||.x.|| = Integral (M,(abs f)) ) & ( for f being PartFunc of X,REAL st f in x holds
Integral (M,(abs f)) = ||.x.|| ) )