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 ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (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 ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (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 ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (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 ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (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 ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x))
let r1, r2 be Element of G; :: thesis: for n being Nat holds ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x))
let n be Nat; :: thesis: ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x))
set g1 = r1 (#) f1;
set g2 = r2 (#) f2;
((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (((cdif ((r1 (#) f1),h)) . (n + 1)) /. x) + (((cdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th22
.= (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (((cdif ((r2 (#) f2),h)) . (n + 1)) /. x) by Th21
.= (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x)) by Th21 ;
hence ((cdif (((r1 (#) f1) + (r2 (#) f2)),h)) . (n + 1)) /. x = (r1 * (((cdif (f1,h)) . (n + 1)) /. x)) + (r2 * (((cdif (f2,h)) . (n + 1)) /. x)) ; :: thesis: verum