theorem Th157: :: ZMODUL01:157

for R being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for a being Element of R
for i being Element of NAT holds - ((Nat-mult-left R) . (i,a)) = (Nat-mult-left R) . (i,(- a))