let S, T be RealNormSpace; 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; 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; 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; ( 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 )
; 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 S1[ Nat] means ( $1 <= n implies diff ((f + g),$1,Z) = (diff (f,$1,Z)) + (diff (g,$1,Z)) );
A3:
S1[ 0 ]
proof
assume
0 <= n
;
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;
verum
end;
A4:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A5:
S1[
i]
;
S1[i + 1]
assume A6:
i + 1
<= n
;
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 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))) . xlet x be
Point of
S;
( 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)))
;
(diff ((f + g),(i + 1),Z)) . x = ((diff (f,(i + 1),Z)) + (diff (g,(i + 1),Z))) . xthen
(((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;
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;
verum
end;
for n being Nat holds S1[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))
; verum