eval ((0_. F_Complex),(1_ F_Complex)) = 0. F_Complex by POLYNOM4:17;
then 1_ F_Complex is_a_root_of 0_. F_Complex by POLYNOM5:def 7;
hence not 0_. F_Complex is Hurwitz by COMPLEX1:6, COMPLFLD:8; :: thesis: verum