0. (RLSp_PFunct X) in L1_Functions M by Lm3;
hence ( RLSp_L1Funct M is strict & RLSp_L1Funct M is Abelian & RLSp_L1Funct M is add-associative & RLSp_L1Funct M is right_zeroed & RLSp_L1Funct M is vector-distributive & RLSp_L1Funct M is scalar-distributive & RLSp_L1Funct M is scalar-associative & RLSp_L1Funct M is scalar-unital ) by Th3; :: thesis: verum