theorem Th30: :: HURWITZ2:30

for p being non constant real with_positive_coefficients Polynomial of F_Complex st [(even_part p),(odd_part p)] is positive & even_part p, odd_part p have_no_common_roots holds
( ( for x being Element of F_Complex st Re x = 0 & eval ((odd_part p),x) <> 0 holds
Re (eval ([(even_part p),(odd_part p)],x)) >= 0 ) & (even_part p) + (odd_part p) is Hurwitz )