( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Lm7, Lm8, Lm9;
hence ex b₁ being non empty multLoopStr st
( b₁ is strict & b₁ is well-unital & b₁ is invertible & b₁ is cancelable ) ; :: thesis: verum