theorem Th62: :: RING_3:63

for R being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer holds (- i) '*' a = - (i '*' a)