:: deftheorem defines RLSp_L1Funct LPSPACE1:def 9 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S holds RLSp_L1Funct M = RLSStruct(# (L1_Functions M),(In ((0. (RLSp_PFunct X)),(L1_Functions M))),(add| ((L1_Functions M),(RLSp_PFunct X))),(Mult_ (L1_Functions M)) #);