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 ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (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 ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (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 ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (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 ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (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 ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x))
let r1, r2 be Element of G; :: thesis: 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))
let n be Nat; :: thesis: ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x))
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
reconsider g1n1 = (fdif ((r1 (#) f1),h)) . (n + 1) as Function of V,W by Th2;
reconsider g2n1 = (fdif ((r2 (#) f2),h)) . (n + 1) as Function of V,W by Th2;
((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (((fdif ((r1 (#) f1),h)) . (n + 1)) /. x) + (((fdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th8
.= (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (((fdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th7
.= (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x)) by Th7 ;
hence ((fdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((fdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((fdif (f2,h)) . (n + 1)) /. x)) ; :: thesis: verum