theorem :: VSDIFF_1:17

for F, G being Field
for V being VectSp of F
for W being VectSp of G
for f1, f2 being Function of V,W
for x, h being Element of V
for n being Nat holds ((bdif ((f1 - f2),h)) . (n + 1)) /. x = (((bdif (f1,h)) . (n + 1)) /. x) - (((bdif (f2,h)) . (n + 1)) /. x)