let f be Polynomial of F_Complex ; :: thesis: ( deg f >= 1 implies for rho being Element of F_Complex st Re rho < 0 & |.(eval f,rho).| < |.(eval (f *' ),rho).| holds
( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz ) )
assume A1: deg f >= 1 ; :: thesis: for rho being Element of F_Complex st Re rho < 0 & |.(eval f,rho).| < |.(eval (f *' ),rho).| holds
( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz )
let rho be Element of F_Complex ; :: thesis: ( Re rho < 0 & |.(eval f,rho).| < |.(eval (f *' ),rho).| implies ( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz ) )
assume A2: ( Re rho < 0 & |.(eval f,rho).| < |.(eval (f *' ),rho).| ) ; :: thesis: ( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz )
reconsider ef = eval f,rho, ef1 = eval (f *' ),rho as Element of F_Complex ;

now

assume A3: (F* f,rho) div (rpoly 1,rho) is Hurwitz ; :: thesis: f is Hurwitz
eval ((ef1 * f) - (ef * (f *' ))),rho = (eval (ef1 * f),rho) - (eval (ef * (f *' )),rho) by POLYNOM4:24
.= (ef1 * (eval f,rho)) - (eval (ef * (f *' )),rho) by POLYNOM5:31
.= (ef1 * (eval f,rho)) - (ef * (eval (f *' ),rho)) by POLYNOM5:31
.= 0. F_Complex by RLVECT_1:28 ;
then rho is_a_root_of (ef1 * f) - (ef * (f *' )) by POLYNOM5:def 6;
then consider t being Polynomial of F_Complex such that
A4: F* f,rho = (rpoly 1,rho) *' t by Th33;
A5: F* f,rho = ((rpoly 1,rho) *' t) + (0_. F_Complex ) by A4, POLYNOM3:29;
- 1 < deg (rpoly 1,rho) by Th27;
then deg (0_. F_Complex ) < deg (rpoly 1,rho) by Th20;
then A6: F* f,rho = ((F* f,rho) div (rpoly 1,rho)) *' (rpoly 1,rho) by A4, A5, Def5;
(1_ F_Complex ) * (rpoly 1,rho) is Hurwitz by A2, Th39;
then rpoly 1,rho is Hurwitz by POLYNOM5:28;
then F* f,rho is Hurwitz by A3, A6, Th41;
hence f is Hurwitz by A1, A2, Th51; :: thesis: verum

end;

hence ( f is Hurwitz iff (F* f,rho) div (rpoly 1,rho) is Hurwitz ) by A1, A2, Th52; :: thesis: verum