theorem :: POLYNOM1:19

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