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