let S, T be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( i <= n - 1 implies diff ((r (#) f),i,Z) is_differentiable_on Z )
assume A4: i <= n - 1 ; :: thesis: 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; :: thesis: verum

end;

hence r (#) f is_differentiable_on n,Z by Th14, A2; :: thesis: verum