:: deftheorem defines L-1-Space LPSPACE1:def 20 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds L-1-Space M = NORMSTR(# the carrier of (Pre-L-Space M), the ZeroF of (Pre-L-Space M), the addF of (Pre-L-Space M), the Mult of (Pre-L-Space M),(L-1-Norm M) #);