let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds ((fdif f,h) . 1) . x = ((Shift f,h) . x) - (f . x)
let f be Function of REAL ,REAL ; :: thesis: ((fdif f,h) . 1) . x = ((Shift f,h) . x) - (f . x)
set f1 = Shift f,h;
((fdif f,h) . 1) . x = ((fdif f,h) . (0 + 1)) . x
.= (fD ((fdif f,h) . 0 ),h) . x by Def6
.= (fD f,h) . x by Def6
.= (f . (x + h)) - (f . x) by Th3
.= ((Shift f,h) . x) - (f . x) by Def2 ;
hence ((fdif f,h) . 1) . x = ((Shift f,h) . x) - (f . x) ; :: thesis: verum