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 & f is_differentiable_on X & f `| X is_continuous_on X holds
f `| 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 & f is_differentiable_on X & f `| X is_continuous_on X holds
f `| Z is_continuous_on Z
let X, Z be Subset of S; :: thesis: ( Z is open & Z c= X & f is_differentiable_on X & f `| X is_continuous_on X implies f `| Z is_continuous_on Z )
assume A1: ( Z is open & Z c= X & f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis: f `| Z is_continuous_on Z
then A2: f `| Z = (f `| X) | Z by Th5;
f `| X is_continuous_on Z by A1, NFCONT_1:23;
hence f `| Z is_continuous_on Z by A2, NFCONT_1:21; :: thesis: verum