let f be PartFunc of REAL,REAL; :: thesis: for I being non empty Interval st f is_differentiable_on_interval I holds
f | I is continuous
let I be non empty Interval; :: thesis: ( f is_differentiable_on_interval I implies f | I is continuous )
assume A1: f is_differentiable_on_interval I ; :: thesis: f | I is continuous
for x being Real st x in dom (f | I) holds
f | I is_continuous_in x

proof

let x be Real; :: thesis: ( x in dom (f | I) implies f | I is_continuous_in x )
assume A2: x in dom (f | I) ; :: thesis: f | I is_continuous_in x

per cases ( x = inf I or x = sup I or ( x <> inf I & x <> sup I ) ) ;

suppose A3: x = inf I ; :: thesis: f | I is_continuous_in x

then f | I is_right_differentiable_in x by A1, A2, Th11;
then A4: (f | I) | (right_closed_halfline x) is_continuous_in x by Th35, FDIFF_3:7;

now :: thesis: for y being Real st y in I holds
y in right_closed_halfline x

let y be Real; :: thesis: ( y in I implies y in right_closed_halfline x )
assume y in I ; :: thesis: y in right_closed_halfline x
then x <= y by A3, XXREAL_2:3;
then y in [.x,+infty.[ by XXREAL_1:236;
hence y in right_closed_halfline x by LIMFUNC1:def 2; :: thesis: verum

end;

then I c= right_closed_halfline x ;
hence f | I is_continuous_in x by A4, RELAT_1:73; :: thesis: verum

end;

suppose A5: x = sup I ; :: thesis: f | I is_continuous_in x

then f | I is_left_differentiable_in x by A1, A2, Th11;
then A6: (f | I) | (left_closed_halfline x) is_continuous_in x by Th36, FDIFF_3:5;

now :: thesis: for y being Real st y in I holds
y in left_closed_halfline x

let y be Real; :: thesis: ( y in I implies y in left_closed_halfline x )
assume y in I ; :: thesis: y in left_closed_halfline x
then y <= x by A5, XXREAL_2:4;
then y in ].-infty,x.] by XXREAL_1:234;
hence y in left_closed_halfline x by LIMFUNC1:def 1; :: thesis: verum

end;

then I c= left_closed_halfline x ;
hence f | I is_continuous_in x by A6, RELAT_1:73; :: thesis: verum

end;

suppose ( x <> inf I & x <> sup I ) ; :: thesis: f | I is_continuous_in x

then x in ].(inf I),(sup I).[ by A2, Th3;
then f is_differentiable_in x by A1, A2, Th11;
hence f | I is_continuous_in x by A2, FDIFF_1:24, FCONT_1:1; :: thesis: verum

end;

end;

end;

hence f | I is continuous by FCONT_1:def 2; :: thesis: verum