theorem Th20: :: HURWITZ2:20

for L being non empty well-unital doubleLoopStr
for p being Polynomial of L st deg p is odd holds
odd_part (Leading-Monomial p) = Leading-Monomial p