theorem Th26: :: GROUP_1A:227

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