let X be set ; :: thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on X holds
f | X is continuous
let f be PartFunc of REAL,REAL; :: thesis: ( f is_differentiable_on X implies f | X is continuous )
assume A1: f is_differentiable_on X ; :: thesis: f | X is continuous
let x be Real; :: according to FCONT_1:def 2 :: thesis: ( not x in dom (f | X) or 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 ) ;
then f | X is_differentiable_in x by A1;
hence f | X is_continuous_in x by Th24; :: thesis: verum