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 (even_part p) <= deg p & deg (odd_part p) <= deg p )
let p be Polynomial of L; :: thesis: ( deg (even_part p) <= deg p & deg (odd_part p) <= deg p )
set e = even_part p;
set o = odd_part p;

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

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

hence ( deg (even_part p) <= deg p & deg (odd_part p) <= deg p ) by Th7; :: thesis: verum

end;

suppose p <> 0_. L ; :: thesis: ( deg (even_part p) <= deg p & deg (odd_part p) <= deg 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 A1: deg pp = max ((deg (even_part p)),(deg (odd_part p))) by Th21, HURWITZ:21;
hence deg (even_part p) <= deg p by XXREAL_0:25; :: thesis: deg (odd_part p) <= deg p
thus deg (odd_part p) <= deg p by A1, XXREAL_0:25; :: thesis: verum

end;

end;