let f be PartFunc of REAL,REAL; :: thesis: for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being natural number st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z be Subset of REAL; :: thesis: for Z1 being open Subset of REAL st Z1 c= Z holds
for n being natural number st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z1 be open Subset of REAL; :: thesis: ( Z1 c= Z implies for n being natural number st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1 )
assume A1: Z1 c= Z ; :: thesis: for n being natural number st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let n be natural number ; :: thesis: ( f is_differentiable_on n + 1,Z implies f is_differentiable_on n + 1,Z1 )
assume A2: f is_differentiable_on n + 1,Z ; :: thesis: f is_differentiable_on n + 1,Z1

now

let k be Element of NAT ; :: thesis: ( k <= (n + 1) - 1 implies (diff (f,Z1)) . k is_differentiable_on Z1 )
assume A3: k <= (n + 1) - 1 ; :: thesis: (diff (f,Z1)) . k is_differentiable_on Z1
(diff (f,Z)) . k is_differentiable_on Z by A2, A3, Def6;
then (diff (f,Z)) . k is_differentiable_on Z1 by A1, FDIFF_1:26;
then A4: ((diff (f,Z)) . k) | Z1 is_differentiable_on Z1 by FDIFF_2:16;
n <= n + 1 by NAT_1:11;
then k <= n + 1 by A3, XXREAL_0:2;
hence (diff (f,Z1)) . k is_differentiable_on Z1 by A1, A2, A4, Th23, Th30; :: thesis: verum

end;

hence f is_differentiable_on n + 1,Z1 by Def6; :: thesis: verum