theorem :: VSDIFF_1:19
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 ((bdif (f,h)) . 1) /. x = (f /. x) - ((Shift (f,(- h))) /. x)