let L be non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for p being Polynomial of L holds deg p = max ((deg (even_part p)),(deg (odd_part p)))
let p be Polynomial of L; :: thesis: deg p = max ((deg (even_part p)),(deg (odd_part p)))
set e = even_part p;
set o = odd_part p;

per cases ( p = 0_. L or p <> 0_. L ) ;

suppose A1: p = 0_. L ; :: thesis: deg p = max ((deg (even_part p)),(deg (odd_part p)))

then ( even_part p = 0_. L & odd_part p = 0_. L ) by Th7;
hence deg p = max ((deg (even_part p)),(deg (odd_part p))) by A1; :: thesis: verum

end;

suppose p <> 0_. L ; :: thesis: deg p = max ((deg (even_part p)),(deg (odd_part p)))

then reconsider pp = p as non zero Polynomial of L by UPROOTS:def 5;
p = (even_part p) + (odd_part p) by Th9;
then deg pp = max ((deg (even_part p)),(deg (odd_part p))) by Th21, HURWITZ:21;
hence deg p = max ((deg (even_part p)),(deg (odd_part p))) ; :: thesis: verum

end;

end;