theorem :: VSDIFF_1:14

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 h being Element of V
for n being Nat st f is constant holds
for x being Element of V holds ((bdif (f,h)) . (n + 1)) /. x = 0. W