:: deftheorem Def20 defines L-1-CNorm LPSPACC1:def 20 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for b₄ being Function of the carrier of (Pre-L-CSpace M),REAL holds
( b₄ = L-1-CNorm M iff for x being Point of (Pre-L-CSpace M) ex f being PartFunc of X,COMPLEX st
( f in x & b₄ . x = Integral (M,(abs f)) ) );