let a, b, c, h be Real; :: thesis: 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)
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = ((a * (x ^2 )) + (b * x)) + c ) implies for x being Real holds (fD f,h) . x = ((((2 * a) * h) * x) + (a * (h ^2 ))) + (b * h) )
assume A1: for x being Real holds f . x = ((a * (x ^2 )) + (b * x)) + c ; :: thesis: for x being Real holds (fD f,h) . x = ((((2 * a) * h) * x) + (a * (h ^2 ))) + (b * h)
let x be Real; :: thesis: (fD f,h) . x = ((((2 * a) * h) * x) + (a * (h ^2 ))) + (b * h)
(fD f,h) . x = (f . (x + h)) - (f . x) by DIFF_1:3
.= (((a * ((x + h) ^2 )) + (b * (x + h))) + c) - (f . x) by A1
.= (((a * ((x + h) ^2 )) + (b * (x + h))) + c) - (((a * (x ^2 )) + (b * x)) + c) by A1
.= ((((2 * a) * h) * x) + (a * (h ^2 ))) + (b * h) ;
hence (fD f,h) . x = ((((2 * a) * h) * x) + (a * (h ^2 ))) + (b * h) ; :: thesis: verum