set M = Trivial-multLoopStr ;
thus Trivial-multLoopStr is right_invertible :: according to ALGSTR_0:def 33 :: thesis: Trivial-multLoopStr is left_invertible

proof

let x be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def 32 :: thesis: x is right_invertible
take x ; :: according to ALGSTR_0:def 28 :: thesis: x * x = 1. Trivial-multLoopStr
thus x * x = 1. Trivial-multLoopStr by STRUCT_0:def 10; :: thesis: verum

end;

let x be Element of Trivial-multLoopStr; :: according to ALGSTR_0:def 31 :: thesis: x is left_invertible
take x ; :: according to ALGSTR_0:def 27 :: thesis: x * x = 1. Trivial-multLoopStr
thus x * x = 1. Trivial-multLoopStr by STRUCT_0:def 10; :: thesis: verum