theorem Th9: :: ALGSTR_1:9

for a, b being Element of Trivial-multLoopStr holds a = b