theorem :: GROUP_1A:37

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