let X be set ; :: thesis: for S, T being non trivial RealNormSpace
for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T st f is_differentiable_on X holds
f is_continuous_on X
let f be PartFunc of S,T; :: thesis: ( f is_differentiable_on X implies f is_continuous_on X )
assume A1: f is_differentiable_on X ; :: thesis: f is_continuous_on X
hence X c= dom f by Def8; :: according to NFCONT_1:def 7 :: thesis: for b₁ being Element of the carrier of S holds
( not b₁ in X or f | X is_continuous_in b₁ )
let x be Point of S; :: thesis: ( not x in X or f | X is_continuous_in x )
assume x in X ; :: thesis: f | X is_continuous_in x
then f | X is_differentiable_in x by A1, Def8;
hence f | X is_continuous_in x by Th49; :: thesis: verum