( Trivial-multLoopStr is well-unital & Trivial-multLoopStr is invertible & Trivial-multLoopStr is cancelable ) by Def14, Lm11, Lm12, Lm13, Lm14, VECTSP_1:def 16;
hence ex b₁ being non empty multLoopStr st
( b₁ is strict & b₁ is well-unital & b₁ is invertible & b₁ is cancelable ) ; :: thesis: verum