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

A2: now

assume A3: Re z < 0 ; :: thesis: x * (rpoly 1,z) is Hurwitz

now

let y be Element of F_Complex ; :: thesis: ( y is_a_root_of x * (rpoly 1,z) implies Re y < 0 )
assume y is_a_root_of x * (rpoly 1,z) ; :: thesis: Re y < 0
then 0. F_Complex = eval (x * (rpoly 1,z)),y by POLYNOM5:def 6
.= x * (eval (rpoly 1,z),y) by POLYNOM5:31
.= x * (y - z) by Th29 ;
then y - z = 0. F_Complex by A1, VECTSP_1:44;
hence Re y < 0 by A3, RLVECT_1:35; :: thesis: verum

end;

hence x * (rpoly 1,z) is Hurwitz by Def8; :: thesis: verum

end;

now

eval (x * (rpoly 1,z)),z = x * (eval (rpoly 1,z),z) by POLYNOM5:31
.= x * (z - z) by Th29
.= x * (0. F_Complex ) by RLVECT_1:28
.= 0. F_Complex by VECTSP_1:36 ;
then A4: z is_a_root_of x * (rpoly 1,z) by POLYNOM5:def 6;
assume x * (rpoly 1,z) is Hurwitz ; :: thesis: Re z < 0
hence Re z < 0 by A4, Def8; :: thesis: verum

end;

hence ( x * (rpoly 1,z) is Hurwitz iff Re z < 0 ) by A2; :: thesis: verum