theorem Th33: :: GROUP_1A:33

for i being Integer
for G being addGroup
for h being Element of G holds
( (i + 1) * h = (i * h) + h & (i + 1) * h = h + (i * h) )