theorem :: GROUP_1A:43

for i being Integer
for A being Abelian addGroup
for a, b being Element of A holds i * (a + b) = (i * a) + (i * b) by ThA37;