theorem Th8: :: POLYNOM4:8
for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds len (- p) = len p