theorem :: VSDIFF_1:11

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 r1, r2 being Element of G
for n being Nat holds ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x))