let S, T be RealNormSpace; for Z being Subset of S
for n being Nat
for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
let Z be Subset of S; for n being Nat
for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
let n be Nat; for r being Real
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
let r be Real; for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
let f be PartFunc of S,T; ( 1 <= n & f is_differentiable_on n,Z implies for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z)) )
assume A1:
( 1 <= n & f is_differentiable_on n,Z )
; for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
A2:
Z is open
by Th18, A1;
defpred S1[ Nat] means ( $1 <= n implies diff ((r (#) f),$1,Z) = r (#) (diff (f,$1,Z)) );
A3:
S1[ 0 ]
proof
assume
0 <= n
;
diff ((r (#) f),0,Z) = r (#) (diff (f,0,Z))
set H =
(diff_SP (S,T)) . 0;
(
(diff_SP (S,T)) . 0 = T &
f | Z = diff (
f,
0,
Z) )
by Def2, Def5;
then
(r (#) f) | Z = r (#) (diff (f,0,Z))
by VFUNCT_1:31;
hence
diff (
(r (#) f),
0,
Z)
= r (#) (diff (f,0,Z))
by Def5;
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 ((r (#) f),(i + 1),Z) = r (#) (diff (f,(i + 1),Z))
A7:
i <= i + 1
by NAT_1:11;
then A8:
i <= n
by A6, XXREAL_0:2;
(i + 1) - 1
<= n - 1
by A6, XREAL_1:9;
then A9:
diff (
f,
i,
Z)
is_differentiable_on Z
by Th14, A1;
then A10:
Z = dom ((diff (f,i,Z)) `| Z)
by NDIFF_1:def 9;
dom (diff (f,i,Z)) = Z
by Th19, A8, A1;
then A11:
Z = dom (r (#) (diff (f,i,Z)))
by VFUNCT_1:def 4;
then
r (#) (diff (f,i,Z)) is_differentiable_on Z
by A2, A9, NDIFF_1:41;
then A12:
dom ((r (#) (diff (f,i,Z))) `| Z) = Z
by NDIFF_1:def 9;
now for x being Point of S st x in dom ((r (#) (diff (f,i,Z))) `| Z) holds
((r (#) (diff (f,i,Z))) `| Z) /. x = r * (((diff (f,i,Z)) `| Z) /. x)let x be
Point of
S;
( x in dom ((r (#) (diff (f,i,Z))) `| Z) implies ((r (#) (diff (f,i,Z))) `| Z) /. x = r * (((diff (f,i,Z)) `| Z) /. x) )assume A13:
x in dom ((r (#) (diff (f,i,Z))) `| Z)
;
((r (#) (diff (f,i,Z))) `| Z) /. x = r * (((diff (f,i,Z)) `| Z) /. x)then
((r (#) (diff (f,i,Z))) `| Z) /. x = r * (diff ((diff (f,i,Z)),x))
by NDIFF_1:41, A9, A2, A11, A12;
hence
((r (#) (diff (f,i,Z))) `| Z) /. x = r * (((diff (f,i,Z)) `| Z) /. x)
by NDIFF_1:def 9, A9, A12, A13;
verum end;
then A14:
(r (#) (diff (f,i,Z))) `| Z = r (#) ((diff (f,i,Z)) `| Z)
by A12, A10, VFUNCT_1:def 4;
A15:
diff_SP (
(i + 1),
S,
T)
= R_NormSpace_of_BoundedLinearOperators (
S,
(diff_SP (i,S,T)))
by Th10;
diff (
(r (#) f),
(i + 1),
Z)
= (diff ((r (#) f),i,Z)) `| Z
by Th13;
hence
diff (
(r (#) f),
(i + 1),
Z)
= r (#) (diff (f,(i + 1),Z))
by Th13, A15, A14, A5, A7, A6, XXREAL_0:2;
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 ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
; verum