for x being Element of F_Complex st x <> 0. F_Complex holds
x * (1_. F_Complex) is Hurwitz