let f be PartFunc of REAL,REAL; :: thesis:
let I be non empty Interval; :: thesis:

hereby :: thesis:

assume A1: f is_differentiable_on_interval I ; :: thesis:
hence I c= dom f ; :: thesis:
thus for x being Real st x in I holds
( ( x = inf I implies f | I is_right_differentiable_in x ) & ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) ) :: thesis:

proof

let x be Real; :: thesis:
assume A2: x in I ; :: thesis:
thus ( x = inf I implies f | I is_right_differentiable_in x ) :: thesis:

proof

assume A3: x = inf I ; :: thesis:
then f is_right_differentiable_in x by A1, A2, Lm5;
hence f | I is_right_differentiable_in x by A1, A2, A3, Th4; :: thesis:

end;

thus ( x = sup I implies f | I is_left_differentiable_in x ) :: thesis:

proof

assume A4: x = sup I ; :: thesis:
then f is_left_differentiable_in x by A1, A2, Lm6;
hence f | I is_left_differentiable_in x by A1, A2, A4, Th5; :: thesis:

end;

assume x in ].(inf I),(sup I).[ ; :: thesis:
then ( inf I < x & x < sup I ) by XXREAL_1:4;
then consider Z being open Subset of REAL such that
A5: ( x in Z & Z c= ].(inf I),(sup I).[ ) by Lm9;
f is_differentiable_on Z by A1, A5, FDIFF_1:26;
hence f is_differentiable_in x by A5, FDIFF_1:9; :: thesis:

end;

assume that
A6: I c= dom f and
A7: for x being Real st x in I holds
( ( x = inf I implies f | I is_right_differentiable_in x ) & ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) ) ; :: thesis:

A8: now :: thesis:

assume inf I = sup I ; :: thesis:
then A9: I = {(inf I)} by XXREAL_2:70;
then A10: inf I in I by ZFMISC_1:31;
then reconsider x = inf I as Real ;
f | I is_right_differentiable_in x by A7, A10;
then consider r being Real such that
A11: ( r > 0 & [.x,(x + r).] c= dom (f | I) ) by FDIFF_3:def 3;
dom (f | I) c= I ;
then A12: [.x,(x + r).] c= I by A11;
A13: x < x + r by A11, XREAL_1:29;
then x + r in {(inf I)} by A12, A9, XXREAL_1:1;
hence contradiction by A13, TARSKI:def 1; :: thesis:

end;

A14: inf I <= sup I by XXREAL_2:40;
A15: ( inf I in I implies f is_right_differentiable_in lower_bound I )

proof

assume A16: inf I in I ; :: thesis:
then inf I = lower_bound I by Lm5;
then f | I is_right_differentiable_in lower_bound I by A16, A7;
hence f is_right_differentiable_in lower_bound I by Th9; :: thesis:

end;

A17: ( sup I in I implies f is_left_differentiable_in upper_bound I )

proof

assume A18: sup I in I ; :: thesis:
then sup I = upper_bound I by Lm6;
then f | I is_left_differentiable_in upper_bound I by A18, A7;
hence f is_left_differentiable_in upper_bound I by Th10; :: thesis:

end;

A19: now :: thesis:

let a be set ; :: thesis:
assume A20: a in ].(inf I),(sup I).[ ; :: thesis:
then reconsider a1 = a as Real ;
( inf I < a1 & a1 < sup I ) by A20, XXREAL_1:4;
hence a in I by XXREAL_2:83; :: thesis:

end;

A21: ].(inf I),(sup I).[ c= I by Th2;
A22: ].(inf I),(sup I).[ c= dom f by A6, A19;
set J = ].(inf I),(sup I).[;
for x being Real st x in ].(inf I),(sup I).[ holds
f | ].(inf I),(sup I).[ is_differentiable_in x

proof

let x be Real; :: thesis:
assume A23: x in ].(inf I),(sup I).[ ; :: thesis:
then f is_differentiable_in x by A7, A21;
then consider N1 being Neighbourhood of x such that
A24: ( N1 c= dom f & ex L being LinearFunc ex R being RestFunc st
for p being Real st p in N1 holds
(f . p) - (f . x) = (L . (p - x)) + (R . (p - x)) ) ;
ex r1 being Real st
( inf I < r1 & r1 < x )

proof

per cases ;

suppose A25: inf I = -infty ; :: thesis:

consider r1 being Real such that
A26: r1 < x by XREAL_1:2;
take r1 ; :: thesis:
thus ( inf I < r1 & r1 < x ) by A25, A26, XXREAL_0:12, XREAL_0:def 1; :: thesis:

end;

suppose A27: inf I <> -infty ; :: thesis:

A28: inf I < x by A23, XXREAL_1:4;
then inf I <> +infty by XXREAL_0:3;
then inf I in REAL by A27, XXREAL_0:14;
then reconsider iI = inf I as Real ;
consider r1 being Real such that
A29: ( iI < r1 & r1 < x ) by A28, XREAL_1:5;
take r1 ; :: thesis:
thus ( inf I < r1 & r1 < x ) by A29; :: thesis:

end;

then consider r1 being Real such that
A30: ( inf I < r1 & r1 < x ) ;
ex r2 being Real st
( x < r2 & r2 < sup I )

proof

per cases ;

suppose A31: sup I = +infty ; :: thesis:

consider r2 being Real such that
A32: x < r2 by XREAL_1:1;
take r2 ; :: thesis:
thus ( x < r2 & r2 < sup I ) by A31, A32, XREAL_0:def 1, XXREAL_0:9; :: thesis:

end;

suppose A33: sup I <> +infty ; :: thesis:

A34: sup I > x by A23, XXREAL_1:4;
then sup I <> -infty by XXREAL_0:5;
then sup I in REAL by A33, XXREAL_0:14;
then reconsider sI = sup I as Real ;
consider r2 being Real such that
A35: ( x < r2 & r2 < sI ) by A34, XREAL_1:5;
take r2 ; :: thesis:
thus ( x < r2 & r2 < sup I ) by A35; :: thesis:

end;

then consider r2 being Real such that
A36: ( x < r2 & r2 < sup I ) ;
A37: ( x - r1 > 0 & r2 - x > 0 ) by A30, A36, XREAL_1:50;
set rr = min ((x - r1),(r2 - x));
reconsider N2 = ].(x - (min ((x - r1),(r2 - x)))),(x + (min ((x - r1),(r2 - x)))).[ as Neighbourhood of x by A37, XXREAL_0:21, RCOMP_1:def 6;
( r1 <= x - (min ((x - r1),(r2 - x))) & x + (min ((x - r1),(r2 - x))) <= r2 ) by XXREAL_0:17, XREAL_1:11, XREAL_1:19;
then A38: ].(x - (min ((x - r1),(r2 - x)))),(x + (min ((x - r1),(r2 - x)))).[ c= ].r1,r2.[ by XXREAL_1:46;
A39: ].r1,r2.[ c= ].(inf I),(sup I).[ by A30, A36, XXREAL_1:46;
consider N being Neighbourhood of x such that
A40: ( N c= N1 & N c= N2 ) by RCOMP_1:17;
( N c= dom f & N c= ].(inf I),(sup I).[ ) by A24, A38, A39, A40;
then N c= (dom f) /\ ].(inf I),(sup I).[ by XBOOLE_1:19;
then A41: N c= dom (f | ].(inf I),(sup I).[) by RELAT_1:61;
consider L being LinearFunc, R being RestFunc such that
A42: for p being Real st p in N1 holds
(f . p) - (f . x) = (L . (p - x)) + (R . (p - x)) by A24;
for p being Real st p in N holds
((f | ].(inf I),(sup I).[) . p) - ((f | ].(inf I),(sup I).[) . x) = (L . (p - x)) + (R . (p - x))

proof

let p be Real; :: thesis:
assume A43: p in N ; :: thesis:
x in N by RCOMP_1:16;
then ( (f | ].(inf I),(sup I).[) . p = f . p & (f | ].(inf I),(sup I).[) . x = f . x ) by A41, A43, FUNCT_1:47;
hence ((f | ].(inf I),(sup I).[) . p) - ((f | ].(inf I),(sup I).[) . x) = (L . (p - x)) + (R . (p - x)) by A42, A43, A40; :: thesis:

end;

hence f | ].(inf I),(sup I).[ is_differentiable_in x by A41; :: thesis:

end;

then f is_differentiable_on ].(inf I),(sup I).[ by A22;
hence f is_differentiable_on_interval I by A6, A14, A15, A17, A8, XXREAL_0:1; :: thesis: