let p be Hurwitz Polynomial of F_Complex; :: thesis: even_part p, odd_part p have_no_common_roots
set e = even_part p;
set o = odd_part p;
let x be Element of F_Complex; :: according to RATFUNC1:def 4 :: thesis: not x is_a_common_root_of even_part p, odd_part p
assume A1: x is_a_common_root_of even_part p, odd_part p ; :: thesis: contradiction
A2: x is_a_root_of (even_part p) + (odd_part p) by A1, RATFUNC1:16;
(even_part p) + (odd_part p) = p by Th9;
then A3: ( Re x < 0 & Re (- x) < 0 ) by A1, Th26, A2, HURWITZ:def 8;
reconsider s = x as Complex ;
Re (- s) = - (Re s) by COMPLEX1:17;
hence contradiction by A3, COMPLFLD:2; :: thesis: verum