theorem Th72: :: POLYNOM9:72

for x being object
for f being FinSequence of F_Complex
for A being set ex i being Integer st
( ( i = 1 or i = - 1 ) & (SignGen (f, the addF of F_Complex,A)) . x = i * (f . x) )