let F be RealNormSpace; :: thesis: for X being set
for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
let X be set ; :: thesis: for f being PartFunc of REAL, the carrier of F st f is_differentiable_on X holds
f | X is continuous
let f be PartFunc of REAL, the carrier of F; :: thesis: ( f is_differentiable_on X implies f | X is continuous )
assume A1: f is_differentiable_on X ; :: thesis: f | X is continuous
for x being Real st x in dom (f | X) holds
f | X is_continuous_in x by A1, Th22;
hence f | X is continuous by NFCONT_3:def 2; :: thesis: verum