for x, z being Element of F_Complex st x <> 0. F_Complex holds
( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 )