let f be Function of REAL,REAL; :: thesis: ( f is differentiable implies f is continuous )
assume f is differentiable ; :: thesis: f is continuous
then f is_differentiable_on REAL by FUNCT_2:def 1;
hence f is continuous by FDIFF_1:25; :: thesis: verum