theorem Th15: :: HURWITZ:15
for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for x being Element of L holds - (x * p) = (- x) * p