:: deftheorem defines L-1-CSpace LPSPACC1:def 21 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-CSpace M = CNORMSTR(# the carrier of (Pre-L-CSpace M), the ZeroF of (Pre-L-CSpace M), the addF of (Pre-L-CSpace M), the Mult of (Pre-L-CSpace M),(L-1-CNorm M) #);