let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S holds
( f is_differentiable_on 1,Z iff ( Z c= dom f & f | Z is_differentiable_on Z ) )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S holds
( f is_differentiable_on 1,Z iff ( Z c= dom f & f | Z is_differentiable_on Z ) )
let Z be Subset of S; :: thesis: ( f is_differentiable_on 1,Z iff ( Z c= dom f & f | Z is_differentiable_on Z ) )

hereby :: thesis: ( Z c= dom f & f | Z is_differentiable_on Z implies f is_differentiable_on 1,Z )

assume A1: f is_differentiable_on 1,Z ; :: thesis: ( Z c= dom f & f | Z is_differentiable_on Z )
hence Z c= dom f ; :: thesis: f | Z is_differentiable_on Z
A2: diff (f,0,Z) is_differentiable_on Z by A1, Th14;
(diff (f,Z)) . 0 = f | Z by Def5;
hence f | Z is_differentiable_on Z by A2, Th7; :: thesis: verum

end;

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

proof

let i be Nat; :: thesis: ( i <= 1 - 1 implies diff (f,i,Z) is_differentiable_on Z )
assume i <= 1 - 1 ; :: thesis: diff (f,i,Z) is_differentiable_on Z
then A4: i = 0 ;
f | Z = diff (f,0,Z) by Def5;
hence diff (f,i,Z) is_differentiable_on Z by A4, A3, Th7; :: thesis: verum

end;

hence f is_differentiable_on 1,Z by A3, Th14; :: thesis: verum