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 n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((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 n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((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 n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)
let f1, f2 be Function of V,W; :: thesis: for x, h being Element of V
for n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)
let x, h be Element of V; :: thesis: for n being Nat holds ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)
let n be Nat; :: thesis: ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x)
defpred S₁[ Nat] means for x being Element of V holds ((fdif ((f1 + f2),h)) . ($1 + 1)) /. x = (((fdif (f1,h)) . ($1 + 1)) /. x) + (((fdif (f2,h)) . ($1 + 1)) /. x);
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: for x being Element of V holds ((fdif ((f1 + f2),h)) . (k + 1)) /. x = (((fdif (f1,h)) . (k + 1)) /. x) + (((fdif (f2,h)) . (k + 1)) /. x) ; :: thesis: S₁[k + 1]
let x be Element of V; :: thesis: ((fdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x = (((fdif (f1,h)) . ((k + 1) + 1)) /. x) + (((fdif (f2,h)) . ((k + 1) + 1)) /. x)
A3: ( ((fdif ((f1 + f2),h)) . (k + 1)) /. x = (((fdif (f1,h)) . (k + 1)) /. x) + (((fdif (f2,h)) . (k + 1)) /. x) & ((fdif ((f1 + f2),h)) . (k + 1)) /. (x + h) = (((fdif (f1,h)) . (k + 1)) /. (x + h)) + (((fdif (f2,h)) . (k + 1)) /. (x + h)) ) by A2;
reconsider fdiff12 = (fdif ((f1 + f2),h)) . (k + 1) as Function of V,W by Th2;
reconsider fdiff2 = (fdif (f2,h)) . (k + 1) as Function of V,W by Th2;
reconsider fdiff1 = (fdif (f1,h)) . (k + 1) as Function of V,W by Th2;
A6: (fD (((fdif (f1,h)) . (k + 1)),h)) /. x = (fD (fdiff1,h)) /. x
.= (((fdif (f1,h)) . (k + 1)) /. (x + h)) - (((fdif (f1,h)) . (k + 1)) /. x) by Th3 ;
A7: (fD (((fdif (f2,h)) . (k + 1)),h)) /. x = (fD (fdiff2,h)) /. x
.= (((fdif (f2,h)) . (k + 1)) /. (x + h)) - (((fdif (f2,h)) . (k + 1)) /. x) by Th3 ;
((fdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x = (fD (((fdif ((f1 + f2),h)) . (k + 1)),h)) /. x by Def6
.= (fdiff12 /. (x + h)) - (fdiff12 /. x) by Th3
.= (((((fdif (f1,h)) . (k + 1)) /. (x + h)) + (((fdif (f2,h)) . (k + 1)) /. (x + h))) - (((fdif (f2,h)) . (k + 1)) /. x)) - (((fdif (f1,h)) . (k + 1)) /. x) by RLVECT_1:27, A3
.= ((((fdif (f1,h)) . (k + 1)) /. (x + h)) + ((((fdif (f2,h)) . (k + 1)) /. (x + h)) - (((fdif (f2,h)) . (k + 1)) /. x))) - (((fdif (f1,h)) . (k + 1)) /. x) by RLVECT_1:28
.= ((((fdif (f2,h)) . (k + 1)) /. (x + h)) - (((fdif (f2,h)) . (k + 1)) /. x)) + ((((fdif (f1,h)) . (k + 1)) /. (x + h)) - (((fdif (f1,h)) . (k + 1)) /. x)) by RLVECT_1:28
.= (((fdif (f1,h)) . ((k + 1) + 1)) /. x) + ((fD (((fdif (f2,h)) . (k + 1)),h)) /. x) by Def6, A6, A7
.= (((fdif (f1,h)) . ((k + 1) + 1)) /. x) + (((fdif (f2,h)) . ((k + 1) + 1)) /. x) by Def6 ;
hence ((fdif ((f1 + f2),h)) . ((k + 1) + 1)) /. x = (((fdif (f1,h)) . ((k + 1) + 1)) /. x) + (((fdif (f2,h)) . ((k + 1) + 1)) /. x) ; :: thesis: verum

end;

B1: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def 1
.= the carrier of V /\ (dom f2) by FUNCT_2:def 1
.= the carrier of V /\ the carrier of V by FUNCT_2:def 1
.= the carrier of V ;
A7: S₁[ 0 ]

proof

let x be Element of V; :: thesis: ((fdif ((f1 + f2),h)) . (0 + 1)) /. x = (((fdif (f1,h)) . (0 + 1)) /. x) + (((fdif (f2,h)) . (0 + 1)) /. x)
((fdif ((f1 + f2),h)) . (0 + 1)) /. x = (fD (((fdif ((f1 + f2),h)) . 0),h)) /. x by Def6
.= (fD ((f1 + f2),h)) /. x by Def6
.= ((f1 + f2) /. (x + h)) - ((f1 + f2) /. x) by Th3
.= ((f1 /. (x + h)) + (f2 /. (x + h))) - ((f1 + f2) /. x) by B1, VFUNCT_1:def 1
.= ((f1 /. (x + h)) + (f2 /. (x + h))) - ((f1 /. x) + (f2 /. x)) by B1, VFUNCT_1:def 1
.= (((f1 /. (x + h)) + (f2 /. (x + h))) - (f2 /. x)) - (f1 /. x) by RLVECT_1:27
.= ((f1 /. (x + h)) + ((f2 /. (x + h)) - (f2 /. x))) - (f1 /. x) by RLVECT_1:28
.= ((f2 /. (x + h)) - (f2 /. x)) + ((f1 /. (x + h)) - (f1 /. x)) by RLVECT_1:28
.= ((fD (f1,h)) /. x) + ((f2 /. (x + h)) - (f2 /. x)) by Th3
.= ((fD (f1,h)) /. x) + ((fD (f2,h)) /. x) by Th3
.= ((fD (((fdif (f1,h)) . 0),h)) /. x) + ((fD (f2,h)) /. x) by Def6
.= ((fD (((fdif (f1,h)) . 0),h)) /. x) + ((fD (((fdif (f2,h)) . 0),h)) /. x) by Def6
.= (((fdif (f1,h)) . (0 + 1)) /. x) + ((fD (((fdif (f2,h)) . 0),h)) /. x) by Def6
.= (((fdif (f1,h)) . (0 + 1)) /. x) + (((fdif (f2,h)) . (0 + 1)) /. x) by Def6 ;
hence ((fdif ((f1 + f2),h)) . (0 + 1)) /. x = (((fdif (f1,h)) . (0 + 1)) /. x) + (((fdif (f2,h)) . (0 + 1)) /. x) ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A1);
hence ((fdif ((f1 + f2),h)) . (n + 1)) /. x = (((fdif (f1,h)) . (n + 1)) /. x) + (((fdif (f2,h)) . (n + 1)) /. x) ; :: thesis: verum