:: deftheorem defines CLSp_L1Funct LPSPACC1:def 10 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds CLSp_L1Funct M = CLSStruct(# (L1_CFunctions M),(In ((0. (CLSp_PFunct X)),(L1_CFunctions M))),(add| ((L1_CFunctions M),(CLSp_PFunct X))),(Mult_ (L1_CFunctions M)) #);