theorem Th66: :: POLYNOM9:66

for m being non trivial Nat
for p being Jpolynom of m, F_Complex
for f being FinSequence of REAL
for xf, cxf being Function of m,F_Complex st xf = FS2XFS f & cxf = FS2XFS (_sqrt f) holds
eval (p,cxf) = eval ((JsqrtSeries p),xf)