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