(Eval p) `| = Eval (poly_diff p) by Th61;
hence (Eval p) `| is differentiable ; :: thesis: verum