theorem ThB37: :: GROUP_1A:238

for G being addGroup
for a, b being Element of G holds {a} * {b} = {(a * b)}