theorem Th60: :: POLYDIFF:60
for n being Nat
for r being Element of F_Real holds Eval (seq (n,r)) = r (#) (#Z n)