theorem Th67: :: GROUP_1A:268

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