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