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
r (#) f is_differentiable_on n,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
r (#) f is_differentiable_on n,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
r (#) f is_differentiable_on n,Z
let r be Real; for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
r (#) f is_differentiable_on n,Z
let f be PartFunc of S,T; ( 1 <= n & f is_differentiable_on n,Z implies r (#) f is_differentiable_on n,Z )
assume A1:
( 1 <= n & f is_differentiable_on n,Z )
; r (#) f is_differentiable_on n,Z
then A2:
Z c= dom (r (#) f)
by VFUNCT_1:def 4;
A3:
Z is open
by Th18, A1;
for i being Nat st i <= n - 1 holds
diff ((r (#) f),i,Z) is_differentiable_on Z
proof
let i be
Nat;
( i <= n - 1 implies diff ((r (#) f),i,Z) is_differentiable_on Z )
assume A4:
i <= n - 1
;
diff ((r (#) f),i,Z) is_differentiable_on Z
set H =
diff_SP (
i,
S,
T);
set f1 =
diff (
f,
i,
Z);
A5:
diff (
f,
i,
Z)
is_differentiable_on Z
by A1, A4, Th14;
(n - 1) - 0 <= (n - 1) + 1
by XREAL_1:7;
then A6:
i <= n
by A4, XXREAL_0:2;
then A7:
diff (
(r (#) f),
i,
Z)
= r (#) (diff (f,i,Z))
by A1, Th24;
dom (diff (f,i,Z)) = Z
by Th19, A6, A1;
then
Z c= dom (r (#) (diff (f,i,Z)))
by VFUNCT_1:def 4;
hence
diff (
(r (#) f),
i,
Z)
is_differentiable_on Z
by A3, A5, A7, NDIFF_1:41;
verum
end;
hence
r (#) f is_differentiable_on n,Z
by Th14, A2; verum