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