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