set M = Trivial-multLoopStr_0 ;
thus Trivial-multLoopStr_0 is almost_right_invertible by STRUCT_0:def 10; :: according to ALGSTR_0:def 40 :: thesis: Trivial-multLoopStr_0 is almost_left_invertible
let x be Element of Trivial-multLoopStr_0; :: according to ALGSTR_0:def 38 :: thesis: ( x <> 0. Trivial-multLoopStr_0 implies x is left_invertible )
assume x <> 0. Trivial-multLoopStr_0 ; :: thesis: x is left_invertible
take x ; :: according to ALGSTR_0:def 27 :: thesis: x * x = 1. Trivial-multLoopStr_0
thus x * x = 1. Trivial-multLoopStr_0 by STRUCT_0:def 10; :: thesis: verum