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

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

assume A1: f is_differentiable_on 2,Z ; :: thesis: ( Z c= dom f & f | Z is_differentiable_on Z & (f | Z) `| Z is_differentiable_on Z )
hence Z c= dom f ; :: thesis: ( f | Z is_differentiable_on Z & (f | Z) `| 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: (f | Z) `| Z is_differentiable_on Z
A3: diff (f,1,Z) is_differentiable_on Z by A1, Th14;
(diff (f,Z)) . 1 = (f | Z) `| Z by Th11;
hence (f | Z) `| Z is_differentiable_on Z by A3, Th7; :: thesis: verum

end;

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

proof

let i be Nat; :: thesis: ( i <= 2 - 1 implies diff (f,i,Z) is_differentiable_on Z )
assume A5: i <= 2 - 1 ; :: thesis: diff (f,i,Z) is_differentiable_on Z

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

suppose A6: i = 1 ; :: thesis: diff (f,i,Z) is_differentiable_on Z

(f | Z) `| Z = diff (f,1,Z) by Th11;
hence diff (f,i,Z) is_differentiable_on Z by A6, A4, Th7; :: thesis: verum

end;

suppose i <> 1 ; :: thesis: diff (f,i,Z) is_differentiable_on Z

then i < 1 by A5, XXREAL_0:1;
then A7: i = 0 by NAT_1:14;
f | Z = diff (f,0,Z) by Def5;
hence diff (f,i,Z) is_differentiable_on Z by A7, A4, Th7; :: thesis: verum

end;

end;

end;

hence f is_differentiable_on 2,Z by Th14, A4; :: thesis: verum