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
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,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
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,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
for i being Nat st i <= n holds
diff ((r (#) f),i,Z) = r (#) (diff (f,i,Z))
let r be Real; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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 S₁[ Nat] means ( $1 <= n implies diff ((r (#) f),$1,Z) = r (#) (diff (f,$1,Z)) );
A3: S₁[ 0 ]

proof

assume 0 <= n ; :: thesis: 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; :: 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 ((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 :: thesis: 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; :: thesis: ( 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) ; :: thesis: ((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; :: thesis: 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; :: 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 ((r (#) f),i,Z) = r (#) (diff (f,i,Z)) ; :: thesis: verum