let f be Polynomial of F_Complex; :: thesis: for z being Element of F_Complex st z <> 0. F_Complex holds
( f is Hurwitz iff z * f is Hurwitz )
let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies ( f is Hurwitz iff z * f is Hurwitz ) )
assume A1: z <> 0. F_Complex ; :: thesis: ( f is Hurwitz iff z * f is Hurwitz )

A2: now

assume A3: f is Hurwitz ; :: thesis: z * f is Hurwitz

now

let x be Element of F_Complex; :: thesis: ( x is_a_root_of z * f implies Re x < 0 )
assume x is_a_root_of z * f ; :: thesis: Re x < 0
then 0. F_Complex = eval ((z * f),x) by POLYNOM5:def 6
.= z * (eval (f,x)) by POLYNOM5:31 ;
then eval (f,x) = 0. F_Complex by A1, VECTSP_1:44;
then x is_a_root_of f by POLYNOM5:def 6;
hence Re x < 0 by A3, Def8; :: thesis: verum

end;

hence z * f is Hurwitz by Def8; :: thesis: verum

end;

now

assume A4: z * f is Hurwitz ; :: thesis: f is Hurwitz

now

let x be Element of F_Complex; :: thesis: ( x is_a_root_of f implies Re x < 0 )
assume A5: x is_a_root_of f ; :: thesis: Re x < 0
eval ((z * f),x) = z * (eval (f,x)) by POLYNOM5:31
.= z * (0. F_Complex) by A5, POLYNOM5:def 6
.= 0. F_Complex by VECTSP_1:36 ;
then x is_a_root_of z * f by POLYNOM5:def 6;
hence Re x < 0 by A4, Def8; :: thesis: verum

end;

hence f is Hurwitz by Def8; :: thesis: verum

end;

hence ( f is Hurwitz iff z * f is Hurwitz ) by A2; :: thesis: verum