let S, E be RealNormSpace; :: thesis: for Z being Subset of S
for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z holds
( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z )
let Z be Subset of S; :: thesis: for u being PartFunc of S,E
for i being Nat st u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z holds
( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z )
let u be PartFunc of S,E; :: thesis: for i being Nat st u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z holds
( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z )
let i be Nat; :: thesis: ( u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z implies ( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z ) )
assume A1: ( u is_differentiable_on i + 1,Z & diff (u,(i + 1),Z) is_continuous_on Z ) ; :: thesis: ( u `| Z is_differentiable_on i,Z & diff ((u `| Z),i,Z) is_continuous_on Z )
hence u `| Z is_differentiable_on i,Z by Th36; :: thesis: diff ((u `| Z),i,Z) is_continuous_on Z
0 <= i by NAT_1:2;
then 0 + 1 <= i + 1 by XREAL_1:7;
then u is_differentiable_on 1,Z by A1, NDIFF_6:17;
then ( Z c= dom u & u | Z is_differentiable_on Z ) by NDIFF_6:15;
then A2: u is_differentiable_on Z ;
then A3: dom (u `| Z) = Z by NDIFF_1:def 9;
A4: diff_SP ((i + 1),S,E) = diff_SP (i,S,(R_NormSpace_of_BoundedLinearOperators (S,E))) by Th30;
(u | Z) `| Z = (u `| Z) | Z by A2, A3, Th4;
hence diff ((u `| Z),i,Z) is_continuous_on Z by A1, A4, Th31; :: thesis: verum