theorem Th69: :: POLYNOM9:69

for m being Ordinal
for Pc being Polynomial of m,F_Complex
for Pr being Polynomial of m,F_Real st Pc = Pr holds
for xc being Function of m,F_Complex
for xr being Function of m,F_Real st xc = xr holds
eval (Pc,xc) = eval (Pr,xr)