theorem ThA37: :: GROUP_1A:35

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