theorem :: ALGSTR_1:10

for a, b being Element of Trivial-multLoopStr holds a * b = 1. Trivial-multLoopStr by Th9;