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