( multEX_0 is commutative & not multEX_0 is degenerated ) by Lm23;
hence ex b₁ being multGroup_0 st
( b₁ is strict & b₁ is commutative ) ; :: thesis: verum