for p0 being Element of (Polynom-Ring F_Real)
for p being Polynomial of F_Real st p0 = p holds
poly_diff p = (Der1 F_Real) . p0