theorem Th70: :: POLYNOM9:70

for m being non trivial Nat
for M being Jpolynom of m, F_Complex
for f being Function of m,F_Real holds
( eval ((Jsqrt M),f) = 0 iff ex A being Subset of ((Seg m) \ {1}) st the addF of F_Complex "**" (SignGen ((_sqrt (XFS2FS (@ f))), the addF of F_Complex,A)) = 0 )