theorem Th4: :: ALGSTR_1:4
for a, b being Element of Trivial-addLoopStr holds a = b