theorem :: HURWITZ2:13

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being Polynomial of L holds (even_part p) - p = - (odd_part p)