( multEX_0 is associative & not multEX_0 is degenerated ) by Lm22;
hence ex b₁ being multLoop_0 st
( b₁ is strict & b₁ is associative & not b₁ is degenerated ) ; :: thesis: verum