let F, G be Field; :: thesis: for V being VectSp of F
for W being VectSp of G
for f being Function of V,W
for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)
let V be VectSp of F; :: thesis: for W being VectSp of G
for f being Function of V,W
for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)
let W be VectSp of G; :: thesis: for f being Function of V,W
for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)
let f be Function of V,W; :: thesis: for x, h being Element of V holds ((fdif (f,h)) . 1) /. x = ((Shift (f,h)) /. x) - (f /. x)
let x, h be Element of V; :: 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