for f, g being Polynomial of F_Complex holds
( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )