:: deftheorem defines F* HURWITZ:def 10 :
for f being Polynomial of F_Complex
for z being Element of F_Complex holds F* (f,z) = ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));