let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for k being positive Real holds
( 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))) #) is Abelian & 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))) #) is add-associative & 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))) #) is right_zeroed & 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))) #) is vector-distributive & 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))) #) is scalar-distributive & 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))) #) is scalar-associative & 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))) #) is scalar-unital )
let S be SigmaField of X; for M being sigma_Measure of S
for k being positive Real holds
( 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))) #) is Abelian & 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))) #) is add-associative & 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))) #) is right_zeroed & 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))) #) is vector-distributive & 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))) #) is scalar-distributive & 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))) #) is scalar-associative & 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))) #) is scalar-unital )
let M be sigma_Measure of S; for k being positive Real holds
( 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))) #) is Abelian & 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))) #) is add-associative & 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))) #) is right_zeroed & 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))) #) is vector-distributive & 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))) #) is scalar-distributive & 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))) #) is scalar-associative & 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))) #) is scalar-unital )
let k be positive Real; ( 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))) #) is Abelian & 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))) #) is add-associative & 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))) #) is right_zeroed & 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))) #) is vector-distributive & 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))) #) is scalar-distributive & 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))) #) is scalar-associative & 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))) #) is scalar-unital )
0. (RLSp_PFunct X) in Lp_Functions (M,k)
by Th23;
hence
( 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))) #) is Abelian & 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))) #) is add-associative & 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))) #) is right_zeroed & 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))) #) is vector-distributive & 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))) #) is scalar-distributive & 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))) #) is scalar-associative & 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))) #) is scalar-unital )
by LPSPACE1:3; verum