Trivial-multLoopStr is associative by Lm10, GROUP_1:def 3;
hence ex b₁ being multLoop st
( b₁ is strict & b₁ is associative ) ; :: thesis: verum