( multEX_0 is well-unital & multEX_0 is multLoop_0-like & not multEX_0 is degenerated ) by Lm17, Lm18, Lm19, Lm20, Lm21, Lm22, Lm23, Th34, STRUCT_0:def 8;
hence ex b₁ being non empty multLoopStr_0 st
( b₁ is strict & b₁ is well-unital & b₁ is multLoop_0-like & not b₁ is degenerated ) ; :: thesis: verum