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 ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. 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 ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)
let W be VectSp of G; :: thesis: for f being Function of V,W
for x, h being Element of V holds ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)
let f be Function of V,W; :: thesis: for x, h being Element of V holds ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)
let x, h be Element of V; :: thesis: ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x)
set f2 = Shift (f,(- (((2 * (1. F)) ") * h)));
set f1 = Shift (f,(((2 * (1. F)) ") * h));
((cdif (f,h)) . 1) /. x = ((cdif (f,h)) . (0 + 1)) /. x
.= (cD (((cdif (f,h)) . 0),h)) /. x by Def8
.= (cD (f,h)) /. x by Def8
.= (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h))) by Th5
.= ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - (f /. (x + (- (((2 * (1. F)) ") * h)))) by Def2
.= ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x) by Def2 ;
hence ((cdif (f,h)) . 1) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x) ; :: thesis: verum