theorem Th72: :: POLYNOM5:72

for p being Polynomial of F_Complex st len p > 2 & |.(p . ((len p) -' 1)).| = 1 holds
for F being FinSequence of REAL st len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval (p,z)).| > |.(p . 0).| + 1