let p be non constant real with_positive_coefficients Polynomial of F_Complex; :: thesis: ( [(even_part p),(odd_part p)] is one_port_function & degree [(even_part p),(odd_part p)] = degree p implies p is Hurwitz )
set e = even_part p;
set o = odd_part p;
set f = [(even_part p),(odd_part p)];
assume A1: ( [(even_part p),(odd_part p)] is one_port_function & degree [(even_part p),(odd_part p)] = degree p ) ; :: thesis: p is Hurwitz
A2: not [(even_part p),(odd_part p)] is zero ;
degree [(even_part p),(odd_part p)] = max ((degree ([(even_part p),(odd_part p)] `1)),(degree ([(even_part p),(odd_part p)] `2))) by A1, Th23;
then [(even_part p),(odd_part p)] is irreducible by A2, RATFUNC1:30;
then (even_part p) + (odd_part p) is Hurwitz by A1, Th30;
hence p is Hurwitz by Th9; :: thesis: verum