:: deftheorem Def9 defines *' HURWITZ:def 9 :
for f, b₂ being Polynomial of F_Complex holds
( b₂ = f *' iff for i being Element of NAT holds b₂ . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') );