( multEX_0 is well-unital & multEX_0 is multLoop_0-like & not multEX_0 is degenerated ) by Lm22, Lm23, Lm24, Lm25, Lm26, Lm27, Lm28, 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