set e = even_part p;
reconsider z = 0 as Element of NAT by ORDINAL1:def 12;
0 <= degree p ;
then A1: p . z <> z by Def10;
(even_part p) . z = p . z by Def1;
then (even_part p) . z <> 0. F_Complex by A1, COMPLFLD:def 1;
hence not even_part p is zero by FUNCOP_1:7; :: thesis: verum