theorem Th17: :: GROUP_1A:218

for G being addGroup
for a being Element of G holds (0_ G) * a = 0_ G