let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S
for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S
for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) )
let Z be Subset of S; :: thesis: for n being Nat holds
( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) )
let n be Nat; :: thesis: ( f is_differentiable_on n,Z iff ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) )

hereby :: thesis: ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) implies f is_differentiable_on n,Z )

assume A1: f is_differentiable_on n,Z ; :: thesis: ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) )
hence Z c= dom f ; :: thesis: for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z

hereby :: thesis: verum

let i be Nat; :: thesis: ( i <= n - 1 implies diff (f,i,Z) is_differentiable_on Z )
assume i <= n - 1 ; :: thesis: diff (f,i,Z) is_differentiable_on Z
then modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z by A1;
hence diff (f,i,Z) is_differentiable_on Z by Def4; :: thesis: verum

end;

end;

assume A2: ( Z c= dom f & ( for i being Nat st i <= n - 1 holds
diff (f,i,Z) is_differentiable_on Z ) ) ; :: thesis: f is_differentiable_on n,Z

now :: thesis: for i being Nat st i <= n - 1 holds
modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z

let i be Nat; :: thesis: ( i <= n - 1 implies modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z )
assume i <= n - 1 ; :: thesis: modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z
then diff (f,i,Z) is_differentiable_on Z by A2;
hence modetrans (((diff (f,Z)) . i),S,(diff_SP (i,S,T))) is_differentiable_on Z by Def4; :: thesis: verum

end;

hence f is_differentiable_on n,Z by A2; :: thesis: verum