let h, x0, x1 be Real; for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
let f, g be Function of REAL,REAL; ( ( for x being Real holds f . x = (cD (g,h)) . x ) implies [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] )
assume A1:
for x being Real holds f . x = (cD (g,h)) . x
; [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
[!f,x0,x1!] =
(((cD (g,h)) . x0) - (f . x1)) / (x0 - x1)
by A1
.=
(((cD (g,h)) . x0) - ((cD (g,h)) . x1)) / (x0 - x1)
by A1
.=
(((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((cD (g,h)) . x1)) / (x0 - x1)
by DIFF_1:5
.=
(((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((g . (x1 + (h / 2))) - (g . (x1 - (h / 2))))) / (x0 - x1)
by DIFF_1:5
.=
[!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
;
hence
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
; verum