theorem :: POLYNOM1:18

for n being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, r being Series of n,L st ( for x being bag of n holds r . x = - (p . x) ) holds
r = - p