let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X holds
for i being Nat st f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X holds
( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z )
let f be PartFunc of S,T; :: thesis: for X, Z being Subset of S st Z is open & Z c= X holds
for i being Nat st f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X holds
( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z )
let X, Z be Subset of S; :: thesis: ( Z is open & Z c= X implies for i being Nat st f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X holds
( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z ) )
assume A1: ( Z is open & Z c= X ) ; :: thesis: for i being Nat st f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X holds
( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z )
let i be Nat; :: thesis: ( f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X implies ( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z ) )
assume A2: ( f is_differentiable_on i,X & diff (f,i,X) is_continuous_on X ) ; :: thesis: ( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z )
then diff (f,i,X) is_continuous_on Z by A1, NFCONT_1:23;
then (diff (f,i,X)) | Z is_continuous_on Z by NFCONT_1:21;
hence ( f is_differentiable_on i,Z & diff (f,i,Z) is_continuous_on Z ) by A1, A2, Th9; :: thesis: verum