let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x)
let f be Function of REAL,REAL; :: thesis: ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x)
set f2 = Shift (f,(- h));
((bdif (f,h)) . 1) . x = ((bdif (f,h)) . (0 + 1)) . x
.= (bD (((bdif (f,h)) . 0),h)) . x by Def7
.= (bD (f,h)) . x by Def7
.= (f . x) - (f . (x - h)) by Th4
.= (f . x) - (f . (x + (- h)))
.= (f . x) - ((Shift (f,(- h))) . x) by Def2 ;
hence ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x) ; :: thesis: verum