let f, g be Polynomial of F_Complex; :: thesis:

A1: now :: thesis:

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

now :: thesis:

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

per cases by A4, VECTSP_1:12;

suppose eval (f,z) = 0. F_Complex ; :: thesis:

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

end;

suppose eval (g,z) = 0. F_Complex ; :: thesis:

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

end;

end;

end;

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

end;

now :: thesis:

assume A5: f *' g is Hurwitz ; :: thesis:

now :: thesis:

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

end;

hence f is Hurwitz ; :: thesis:

now :: thesis:

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

end;

hence g is Hurwitz ; :: thesis:

end;

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