set o = odd_part p;
0 + 1 <= degree p by INT_1:7, RATFUNC1:def 2;
then A1: p . 1 <> 0 by Def10;
(odd_part p) . 1 = p . 1 by Def2, Lm1;
then (odd_part p) . 1 <> 0. F_Complex by A1, COMPLFLD:def 1;
hence not odd_part p is zero by FUNCOP_1:7; :: thesis: verum