theorem Th16: :: HURWITZ2:16

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