let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis:
let p be non zero Polynomial of L; :: thesis:
set e = even_part p;
set o = odd_part p;

per cases ;

suppose A1: ( odd_part p = 0_. L or even_part p = 0_. L ) ; :: thesis:

then A2: ( deg (odd_part p) = - 1 or deg (even_part p) = - 1 ) by HURWITZ:20;
A3: (0_. L) + (0_. L) = 0_. L by POLYNOM3:28;

now :: thesis:

per cases by A1;

case odd_part p = 0_. L ; :: thesis:

then even_part p <> 0_. L by A3, Th9;
hence deg (even_part p) <> deg (odd_part p) by A2, HURWITZ:20; :: thesis:

end;

case even_part p = 0_. L ; :: thesis:

then odd_part p <> 0_. L by A3, Th9;
hence deg (even_part p) <> deg (odd_part p) by A2, HURWITZ:20; :: thesis:

end;

end;

end;

hence deg (even_part p) <> deg (odd_part p) ; :: thesis:

end;

suppose ( odd_part p <> 0_. L & even_part p <> 0_. L ) ; :: thesis:

then reconsider e = even_part p, o = odd_part p as non zero Polynomial of L by UPROOTS:def 5;
reconsider de = degree e as Element of NAT by ORDINAL1:def 12;
reconsider deo = degree o as Element of NAT by ORDINAL1:def 12;

now :: thesis:

assume A4: deg e = deg o ; :: thesis:
(degree e) + 1 = len e ;
then A5: e . de <> 0. L by ALGSEQ_1:10;
(degree o) + 1 = len o ;
then A6: o . deo <> 0. L by ALGSEQ_1:10;

now :: thesis:

per cases ;

case degree e is even ; :: thesis:

hence contradiction by A6, A4, Def2; :: thesis:

end;

case degree e is odd ; :: thesis:

hence contradiction by A5, Def1; :: thesis:

end;

end;

end;

hence contradiction ; :: thesis:

end;

hence deg (even_part p) <> deg (odd_part p) ; :: thesis:

end;

end;