theorem :: HURWITZ2:11

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