theorem Th3: :: POLYRED:3

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