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 & diff ((g `| Z),n,Z) is_continuous_on Z holds
( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on 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 & diff ((g `| Z),n,Z) is_continuous_on Z holds
( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on 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 & diff ((g `| Z),n,Z) is_continuous_on Z holds
( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on Z )
let g be PartFunc of E,F; :: thesis: ( g `| Z is_differentiable_on n,Z & g is_differentiable_on Z & diff ((g `| Z),n,Z) is_continuous_on Z implies ( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on Z ) )
assume A1: ( g `| Z is_differentiable_on n,Z & g is_differentiable_on Z & diff ((g `| Z),n,Z) is_continuous_on Z ) ; :: thesis: ( g is_differentiable_on n + 1,Z & diff (g,(n + 1),Z) is_continuous_on Z )
hence g is_differentiable_on n + 1,Z by Th32; :: thesis: diff (g,(n + 1),Z) is_continuous_on Z
dom (g `| Z) = Z by A1, NDIFF_1:def 9;
then A2: (g `| Z) | Z = (g | Z) `| Z by A1, Th4;
diff (g,(n + 1),Z) = diff ((g `| Z),n,Z) by A2, Th31;
hence diff (g,(n + 1),Z) is_continuous_on Z by A1, Th30; :: thesis: verum