let S, T be RealNormSpace; :: thesis: for Z being Subset of S
for n being Nat
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_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 )
let Z be Subset of S; :: thesis: for n being Nat
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_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 )
let n be Nat; :: 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_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 )
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_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 ) )
assume A1: ( 1 <= n & f is_differentiable_on n,Z ) ; :: thesis: for i being Nat st i <= n holds
( (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 )
let i be Nat; :: thesis: ( i <= n implies ( (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 ) )
assume A2: i <= n ; :: thesis: ( (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 )
diff_SP (i,S,T) is RealNormSpace ;
hence (diff_SP (S,T)) . i is RealNormSpace ; :: thesis: ( (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) & dom (diff (f,i,Z)) = Z )
diff (f,i,Z) is PartFunc of S,(diff_SP (i,S,T)) ;
hence (diff (f,Z)) . i is PartFunc of S,(diff_SP (i,S,T)) ; :: thesis: dom (diff (f,i,Z)) = Z

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: dom (diff (f,i,Z)) = Z

then f | Z = (diff (f,Z)) . i by Def5;
hence dom (diff (f,i,Z)) = Z by RELAT_1:62, A1; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: dom (diff (f,i,Z)) = Z

then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
A3: diff (f,(i1 + 1),Z) = (diff (f,i1,Z)) `| Z by Th13;
diff (f,i1,Z) is_differentiable_on Z by A1, XREAL_1:9, A2, Th14;
hence dom (diff (f,i,Z)) = Z by A3, NDIFF_1:def 9; :: thesis: verum

end;

end;