theorem :: ALGSTR_1:5

for a, b being Element of Trivial-addLoopStr holds a + b = 0. Trivial-addLoopStr by Th4;