theorem :: VSDIFF_1:26
for F, G being Field
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)