theorem Th38: :: GROUP_1A:36

for i, j being Integer
for G being addGroup
for g, h being Element of G st g + h = h + g holds
(i * g) + (j * h) = (j * h) + (i * g)