theorem :: DIFF_2:31

for h, a, b, c being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)