theorem Th29: :: GROUP_1A:29

for i being Integer
for G being addGroup
for h being Element of G st i <= 0 holds
i * h = - (|.i.| * h)