let x be Element of F_Complex ; :: thesis: ( x <> 0. F_Complex implies x * (1_. F_Complex ) is Hurwitz )
assume A1: x <> 0. F_Complex ; :: thesis: x * (1_. F_Complex ) is Hurwitz
set p = x * (1_. F_Complex );

now

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 6;
eval (x * (1_. F_Complex )),z = x * (eval (1_. F_Complex ),z) by POLYNOM5:31
.= x * (1_ F_Complex ) by POLYNOM4:21 ;
hence Re z < 0 by A1, A2, VECTSP_1:def 13; :: thesis: verum

end;

hence x * (1_. F_Complex ) is Hurwitz by Def8; :: thesis: verum