theorem :: GROUP_1A:30

for i being Integer
for G being addGroup holds i * (0_ G) = 0_ G