theorem Th4: :: ALGSTR_1:4

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