for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S ex NORM being Function of the carrier of (Pre-L-CSpace M),REAL st
for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & NORM . x = Integral (M,(abs f)) )