:: deftheorem Def8 defines real HURWITZ2:def 8 :
for p being Polynomial of F_Complex holds
( p is real iff for i being Nat holds p . i is Real );