theorem Th61: :: POLYDIFF:61

for p being Polynomial of F_Real holds (Eval p) `| = Eval (poly_diff p)