theorem Th31: :: E_TRANS1:31

for p being Element of the carrier of (Polynom-Ring F_Real) holds (Eval (~ p)) `| = Eval (~ ((Der1 F_Real) . p))