theorem Th32: :: GROUP_1A:32

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