theorem Th9: :: ALGSTR_1:9
for a, b being Element of Trivial-multLoopStr holds a = b