let h, a, b, c 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 (cD (f,h)) . x = (((2 * a) * h) * x) + (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 (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) )

assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; :: thesis: for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)

let x be Real; :: thesis: (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)

(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5

.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (f . (x - (h / 2))) by A1

.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (((a * ((x - (h / 2)) ^2)) + (b * (x - (h / 2)))) + c) by A1

.= (((2 * a) * h) * x) + (b * h) ;

hence (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) ; :: thesis: verum

for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (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 (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) )

assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; :: thesis: for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)

let x be Real; :: thesis: (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)

(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5

.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (f . (x - (h / 2))) by A1

.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (((a * ((x - (h / 2)) ^2)) + (b * (x - (h / 2)))) + c) by A1

.= (((2 * a) * h) * x) + (b * h) ;

hence (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) ; :: thesis: verum