take Trivial-multLoopStr ; :: thesis: ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & not Trivial-multLoopStr is empty & Trivial-multLoopStr is trivial )
thus ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & not Trivial-multLoopStr is empty & Trivial-multLoopStr is trivial ) ; :: thesis: verum