theorem Th17: :: POLYNOM1:17

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