let f, g be Polynomial of F_Complex; :: thesis: ( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )

A1: now :: thesis: ( f is Hurwitz & g is Hurwitz implies f *' g is Hurwitz )

assume that
A2: f is Hurwitz and
A3: g is Hurwitz ; :: thesis: f *' g is Hurwitz

now :: thesis: for z being Element of F_Complex st z is_a_root_of f *' g holds
Re z < 0

let z be Element of F_Complex; :: thesis: ( z is_a_root_of f *' g implies Re b₁ < 0 )
assume z is_a_root_of f *' g ; :: thesis: Re b₁ < 0
then A4: 0. F_Complex = eval ((f *' g),z) by POLYNOM5:def 7
.= (eval (f,z)) * (eval (g,z)) by POLYNOM4:24 ;

per cases ( eval (f,z) = 0. F_Complex or eval (g,z) = 0. F_Complex ) by A4, VECTSP_1:12;

suppose eval (f,z) = 0. F_Complex ; :: thesis: Re b₁ < 0

then z is_a_root_of f by POLYNOM5:def 7;
hence Re z < 0 by A2; :: thesis: verum

end;

suppose eval (g,z) = 0. F_Complex ; :: thesis: Re b₁ < 0

then z is_a_root_of g by POLYNOM5:def 7;
hence Re z < 0 by A3; :: thesis: verum

end;

end;

end;

hence f *' g is Hurwitz ; :: thesis: verum

end;

now :: thesis: ( f *' g is Hurwitz implies ( f is Hurwitz & g is Hurwitz ) )

assume A5: f *' g is Hurwitz ; :: thesis: ( f is Hurwitz & g is Hurwitz )

now :: thesis: for z being Element of F_Complex st z is_a_root_of f holds
Re z < 0

let z be Element of F_Complex; :: thesis: ( z is_a_root_of f implies Re z < 0 )
assume z is_a_root_of f ; :: thesis: Re z < 0
then z is_a_root_of f *' g by Lm12;
hence Re z < 0 by A5; :: thesis: verum

end;

hence f is Hurwitz ; :: thesis: g is Hurwitz

now :: thesis: for z being Element of F_Complex st z is_a_root_of g holds
Re z < 0

let z be Element of F_Complex; :: thesis: ( z is_a_root_of g implies Re z < 0 )
assume z is_a_root_of g ; :: thesis: Re z < 0
then z is_a_root_of f *' g by Lm12;
hence Re z < 0 by A5; :: thesis: verum

end;

hence g is Hurwitz ; :: thesis: verum

end;

hence ( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) ) by A1; :: thesis: verum