( multEX_0 is well-unital & multEX_0 is multLoop_0-like & not multEX_0 is degenerated ) by Lm16, Lm17, Lm18, Lm19, Lm20, Lm21, Th14;
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