eval ((0_. F_Complex),(1_ F_Complex)) = 0. F_Complex by POLYNOM4:20;
then 1_ F_Complex is_a_root_of 0_. F_Complex by POLYNOM5:def 6;
hence not 0_. F_Complex is Hurwitz by Def8, COMPLEX1:15, COMPLFLD:10; :: thesis: verum