let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 LmDef1Lp;
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; :: thesis: verum