theorem :: DIFF_3:45
for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(fD (f,h)) . x = ((2 * x) * h) + (h ^2)