take Trivial-multLoopStr ; :: thesis: ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element )
thus ( Trivial-multLoopStr is invertible & Trivial-multLoopStr is mult-cancelable & Trivial-multLoopStr is strict & Trivial-multLoopStr is 1 -element ) ; :: thesis: verum