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

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