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 number ; :: 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 ) by RELAT_1:57, XREAL_0:def 1;
then f | X is_differentiable_in x by A1, Def7;
hence f | X is_continuous_in x by Th32; :: thesis: verum