let F be non trivial 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

now

let x be real number ; :: thesis: ( x in dom (f | X) implies f | X is_continuous_in x )
assume x in dom (f | X) ; :: thesis: f | X is_continuous_in x
then ( x is Real & x in X ) by RELAT_1:57, XREAL_0:def 1;
then A2: f | X is_differentiable_in x by A1, Def5;
x is Real by XREAL_0:def 1;
hence f | X is_continuous_in x by A2, Th22; :: thesis: verum

end;

hence f | X is continuous by NFCONT_3:def 2; :: thesis: verum