let E, F be RealNormSpace; :: thesis: for n being Nat
for Z being Subset of E
for g being PartFunc of E,F st g `| Z is_differentiable_on n,Z & g is_differentiable_on Z holds
g is_differentiable_on n + 1,Z
let n be Nat; :: thesis: for Z being Subset of E
for g being PartFunc of E,F st g `| Z is_differentiable_on n,Z & g is_differentiable_on Z holds
g is_differentiable_on n + 1,Z
let Z be Subset of E; :: thesis: for g being PartFunc of E,F st g `| Z is_differentiable_on n,Z & g is_differentiable_on Z holds
g is_differentiable_on n + 1,Z
let g be PartFunc of E,F; :: thesis: ( g `| Z is_differentiable_on n,Z & g is_differentiable_on Z implies g is_differentiable_on n + 1,Z )
assume that
A1: g `| Z is_differentiable_on n,Z and
A2: g is_differentiable_on Z ; :: thesis: g is_differentiable_on n + 1,Z
set f = g `| Z;
A3: dom (g `| Z) = Z by A2, NDIFF_1:def 9;
A4: (g `| Z) | Z = (g | Z) `| Z by A2, A3, Th4;
for i being Nat st i <= (n + 1) - 1 holds
diff (g,i,Z) is_differentiable_on Z

proof

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

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

suppose A6: i = 0 ; :: thesis: diff (g,i,Z) is_differentiable_on Z

A7: diff_SP (i,E,F) = F by A6, NDIFF_6:7;
diff (g,i,Z) = g | Z by A6, NDIFF_6:11;
hence diff (g,i,Z) is_differentiable_on Z by A2, A7, RELAT_1:62; :: thesis: verum

end;

suppose i <> 0 ; :: thesis: diff (g,i,Z) is_differentiable_on Z

then 1 - 1 <= i - 1 by XREAL_1:9, NAT_1:14;
then i - 1 in NAT by INT_1:3;
then reconsider j = i - 1 as Nat ;
A8: diff (g,(j + 1),Z) = diff ((g `| Z),j,Z) by A4, Th31;
diff ((g `| Z),j,Z) is_differentiable_on Z by A1, A5, XREAL_1:9, NDIFF_6:14;
hence diff (g,i,Z) is_differentiable_on Z by A8, Th30; :: thesis: verum

end;

end;

end;

hence g is_differentiable_on n + 1,Z by A2, NDIFF_6:14; :: thesis: verum