let x be Element of F_Complex; :: thesis: ( x <> 0. F_Complex implies x * (1_. F_Complex) is Hurwitz )
set p = x * (1_. F_Complex);
assume A1: x <> 0. F_Complex ; :: thesis: x * (1_. F_Complex) is Hurwitz
now :: thesis: for z being Element of F_Complex st z is_a_root_of x * (1_. F_Complex) holds
Re z < 0
let z be Element of F_Complex; :: thesis: ( z is_a_root_of x * (1_. F_Complex) implies Re z < 0 )
assume z is_a_root_of x * (1_. F_Complex) ; :: thesis: Re z < 0
then A2: eval ((x * (1_. F_Complex)),z) = 0. F_Complex by POLYNOM5:def 7;
eval ((x * (1_. F_Complex)),z) = x * (eval ((1_. F_Complex),z)) by POLYNOM5:30
.= x * (1_ F_Complex) by POLYNOM4:18 ;
hence Re z < 0 by A1, A2; :: thesis: verum
end;
hence x * (1_. F_Complex) is Hurwitz ; :: thesis: verum