let f be Polynomial of F_Complex; :: thesis: ( f is Hurwitz implies for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval (f,x)).| )
assume A1: f is Hurwitz ; :: thesis: for x being Element of F_Complex st Re x >= 0 holds
0 < |.(eval (f,x)).|
let x be Element of F_Complex; :: thesis: ( Re x >= 0 implies 0 < |.(eval (f,x)).| )
assume A2: Re x >= 0 ; :: thesis: 0 < |.(eval (f,x)).|

now

assume eval (f,x) = 0. F_Complex ; :: thesis: contradiction
then x is_a_root_of f by POLYNOM5:def 6;
hence contradiction by A1, A2, Def8; :: thesis: verum

end;

hence 0 < |.(eval (f,x)).| by COMPLEX1:47, COMPLFLD:7; :: thesis: verum