let S, T be RealNormSpace; :: thesis: for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z))
let Z be Subset of S; :: thesis: for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z))
let n be Nat; :: thesis: for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z))
let f, g be PartFunc of S,T; :: thesis: ( 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z implies for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z)) )
assume A1: ( 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z ) ; :: thesis: for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z))
then A2: Z is open by Th18;
defpred S₁[ Nat] means ( $1 <= n implies diff ((f + g),$1,Z) = (diff (f,$1,Z)) + (diff (g,$1,Z)) );
A3: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis: diff ((f + g),0,Z) = (diff (f,0,Z)) + (diff (g,0,Z))
( diff_SP (0,S,T) = T & f | Z = diff (f,0,Z) & g | Z = diff (g,0,Z) & diff ((f + g),0,Z) = (f + g) | Z ) by Def2, Def5;
hence diff ((f + g),0,Z) = (diff (f,0,Z)) + (diff (g,0,Z)) by VFUNCT_1:27; :: thesis: verum

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume A6: i + 1 <= n ; :: thesis: diff ((f + g),(i + 1),Z) = (diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))
then (i + 1) - 1 <= n - 1 by XREAL_1:9;
then A7: ( diff (f,i,Z) is_differentiable_on Z & diff (g,i,Z) is_differentiable_on Z ) by Th14, A1;
A8: i <= i + 1 by NAT_1:11;
then A9: i <= n by A6, XXREAL_0:2;
set f0 = diff (f,i,Z);
set g0 = diff (g,i,Z);
A10: ( (diff_SP (S,T)) . i is RealNormSpace & (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) & dom (diff (f,i,Z)) = Z ) by Th19, A9, A1;
A11: ( (diff_SP (S,T)) . i is RealNormSpace & (diff (g,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) & dom (diff (g,i,Z)) = Z ) by Th19, A9, A1;
Z = (dom (diff (f,i,Z))) /\ Z by A10;
then A12: Z = dom ((diff (f,i,Z)) + (diff (g,i,Z))) by A11, VFUNCT_1:def 1;
then (diff (f,i,Z)) + (diff (g,i,Z)) is_differentiable_on Z by A2, A7, NDIFF_1:39;
then A13: dom (((diff (f,i,Z)) + (diff (g,i,Z))) `| Z) = Z by NDIFF_1:def 9;
A14: ( (diff (f,i,Z)) `| Z = diff (f,(i + 1),Z) & (diff (g,i,Z)) `| Z = diff (g,(i + 1),Z) & diff ((f + g),(i + 1),Z) = (diff ((f + g),i,Z)) `| Z ) by Th13;
A15: ( dom ((diff (f,i,Z)) `| Z) = Z & dom ((diff (g,i,Z)) `| Z) = Z ) by A7, NDIFF_1:def 9;
then A16: ( dom (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) = Z /\ Z & dom ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) = Z /\ Z ) by A14, VFUNCT_1:def 1;

now :: thesis: for x being Point of S st x in dom ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) holds
(diff ((f + g),(i + 1),Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . x

let x be Point of S; :: thesis: ( x in dom ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) implies (diff ((f + g),(i + 1),Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . x )
assume A17: x in dom ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) ; :: thesis: (diff ((f + g),(i + 1),Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . x
then (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) . x = (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) /. x by A16, PARTFUN1:def 6;
then A18: (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) . x = (((diff (f,i,Z)) `| Z) /. x) + (((diff (g,i,Z)) `| Z) /. x) by A17, A16, VFUNCT_1:def 1;
( ((diff (f,i,Z)) `| Z) /. x = (diff (f,(i + 1),Z)) . x & ((diff (g,i,Z)) `| Z) /. x = (diff (g,(i + 1),Z)) . x ) by A16, A17, A14, A15, PARTFUN1:def 6;
then ( ((diff (f,i,Z)) `| Z) /. x = (diff (f,(i + 1),Z)) /. x & ((diff (g,i,Z)) `| Z) /. x = (diff (g,(i + 1),Z)) /. x ) by A16, A17, A14, A15, PARTFUN1:def 6;
then (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) . x = ((diff (f,(i + 1),Z)) /. x) + ((diff (g,(i + 1),Z)) /. x) by A18, Th10;
then (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) /. x by A17, VFUNCT_1:def 1;
then A19: ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . x = (((diff (f,i,Z)) `| Z) + ((diff (g,i,Z)) `| Z)) . x by A17, PARTFUN1:def 6;
(((diff (f,i,Z)) + (diff (g,i,Z))) `| Z) /. x = (diff ((diff (f,i,Z)),x)) + (diff ((diff (g,i,Z)),x)) by NDIFF_1:39, A7, A2, A12, A16, A17;
then A20: (((diff (f,i,Z)) + (diff (g,i,Z))) `| Z) /. x = (((diff (f,i,Z)) `| Z) /. x) + (diff ((diff (g,i,Z)),x)) by NDIFF_1:def 9, A7, A16, A17;
(diff ((f + g),(i + 1),Z)) . x = (((diff (f,i,Z)) + (diff (g,i,Z))) `| Z) /. x by A14, A5, A8, A16, A13, A17, PARTFUN1:def 6, A6, XXREAL_0:2;
hence (diff ((f + g),(i + 1),Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . x by A18, A19, A20, NDIFF_1:def 9, A7, A16, A17; :: thesis: verum

end;

hence diff ((f + g),(i + 1),Z) = (diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z)) by A16, A13, A14, A8, A5, A6, XXREAL_0:2, PARTFUN1:5; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence for i being Nat st i <= n holds
diff ((f + g),i,Z) = (diff (f,i,Z)) + (diff (g,i,Z)) ; :: thesis: verum