Trivial-multLoopStr is commutative by Lm14, GROUP_1:def 12;
hence ex b₁ being multGroup st
( b₁ is strict & b₁ is commutative ) ; :: thesis: verum