theorem Th24: :: GROUP_1A:225

for G being addGroup
for a, g, h being Element of G holds (a * g) * h = a * (g + h)