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