for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz holds
for x being Element of F_Complex holds
( ( Re x < 0 implies |.(eval (f,x)).| < |.(eval ((f *'),x)).| ) & ( Re x > 0 implies |.(eval (f,x)).| > |.(eval ((f *'),x)).| ) & ( Re x = 0 implies |.(eval (f,x)).| = |.(eval ((f *'),x)).| ) )