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 (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))
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 (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))
let W be VectSp of G; :: thesis: for f being Function of V,W
for x, h being Element of V holds (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))
let f be Function of V,W; :: thesis: for x, h being Element of V holds (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))
let x, h be Element of V; :: thesis: (cD (f,h)) /. x = (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h)))
dom ((Shift (f,(((2 * (1. F)) ") * h))) - (Shift (f,(- (((2 * (1. F)) ") * h))))) = the carrier of V by FUNCT_2:def 1;
hence (cD (f,h)) /. x = ((Shift (f,(((2 * (1. F)) ") * h))) /. x) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x) by VFUNCT_1:def 2
.= (f /. (x + (((2 * (1. F)) ") * h))) - ((Shift (f,(- (((2 * (1. F)) ") * h)))) /. x) by Def2
.= (f /. (x + (((2 * (1. F)) ") * h))) - (f /. (x - (((2 * (1. F)) ") * h))) by Def2 ;
:: thesis: verum