theorem Th9: :: POLYRED:9

for X being set
for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Series of X,L
for a being Element of L holds
( - (a * p) = (- a) * p & - (a * p) = a * (- p) )