theorem Th14: :: VSDIFF_1:15

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
for r being Element of G
for n being Nat holds ((bdif ((r (#) f),h)) . (n + 1)) /. x = r * (((bdif (f,h)) . (n + 1)) /. x)