let f be PartFunc of REAL,REAL; for Z being Subset of REAL
for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z be Subset of REAL; for Z1 being open Subset of REAL st Z1 c= Z holds
for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let Z1 be open Subset of REAL; ( Z1 c= Z implies for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1 )
assume A1:
Z1 c= Z
; for n being Nat st f is_differentiable_on n + 1,Z holds
f is_differentiable_on n + 1,Z1
let n be Nat; ( f is_differentiable_on n + 1,Z implies f is_differentiable_on n + 1,Z1 )
assume A2:
f is_differentiable_on n + 1,Z
; f is_differentiable_on n + 1,Z1
now for k being Nat st k <= (n + 1) - 1 holds
(diff (f,Z1)) . k is_differentiable_on Z1let k be
Nat;
( k <= (n + 1) - 1 implies (diff (f,Z1)) . k is_differentiable_on Z1 )assume A3:
k <= (n + 1) - 1
;
(diff (f,Z1)) . k is_differentiable_on Z1
(diff (f,Z)) . k is_differentiable_on Z
by A2, A3;
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;
verum end;
hence
f is_differentiable_on n + 1,Z1
; verum