theorem :: NIVEN:45

for L being non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being Polynomial of L holds LC p = - (LC (- p))