let F, G be Field; :: thesis: 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 ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let V be VectSp of F; :: thesis: 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 ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let W be VectSp of G; :: thesis: 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 ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let f1, f2 be Function of V,W; :: thesis: for x, h being Element of V
for r1, r2 being Element of G
for n being Nat holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let x, h be Element of V; :: thesis: for r1, r2 being Element of G
for n being Nat holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let r1, r2 be Element of G; :: thesis: for n being Nat holds ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
let n be Nat; :: thesis: ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x))
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (((bdif ((r1 (#) f1),h)) . (n + 1)) /. x) + (((bdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th15
.= (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (((bdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th14
.= (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x)) by Th14 ;
hence ((bdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((bdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((bdif (f2,h)) . (n + 1)) /. x)) ; :: thesis: verum