theorem Th23: :: GROUP_1A:224

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