theorem Th1: :: POLYRED:1

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