:: deftheorem defines RLSp_LpFunct LPSPACE2:def 3 :
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds RLSp_LpFunct (M,k) = RLSStruct(# (Lp_Functions (M,k)),(In ((0. (RLSp_PFunct X)),(Lp_Functions (M,k)))),(add| ((Lp_Functions (M,k)),(RLSp_PFunct X))),(Mult_ (Lp_Functions (M,k))) #);