let S, T be RealNormSpace; :: thesis:
let f be PartFunc of S,T; :: thesis:
let Z be Subset of S; :: thesis:

hereby :: thesis:

assume A1: f is_differentiable_on 2,Z ; :: thesis:
hence Z c= dom f ; :: thesis:
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:
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:

end;

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

proof

let i be Nat; :: thesis:
assume A5: i <= 2 - 1 ; :: thesis:

per cases ;

suppose A6: i = 1 ; :: thesis:

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

end;

suppose i <> 1 ; :: thesis:

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:

end;

end;

end;

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