theorem Th6: :: POLYRED:6

for n being Ordinal
for L being non trivial right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L holds
( - (p *' q) = (- p) *' q & - (p *' q) = p *' (- q) )