let h, a, b, c be 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)
let f be Function of REAL,REAL; ( ( 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
; for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
let x be Real; (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)
; verum