let f be PartFunc of REAL , REAL ; :: thesis: for x0 being Real st f is_differentiable_in x0 holds
( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 )
let x0 be Real; :: thesis: ( f is_differentiable_in x0 implies ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 ) )
assume A1: f is_differentiable_in x0 ; :: thesis: ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 )
A2: diff f,x0 = diff f,x0 ;
consider N being Neighbourhood of x0 such that
A3: N c= dom f by A1, FDIFF_2:11;
consider g1 being real number such that
A4: ( g1 > 0 & N = ].(x0 - g1),(x0 + g1).[ ) by RCOMP_1:def 7;
A5: g1 / 2 > 0 by A4, XREAL_1:141;
A6: g1 > g1 / 2 by A4, XREAL_1:218;
A7: ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f )

proof

take r = g1 / 2; :: thesis: ( r > 0 & [.x0,(x0 + r).] c= dom f )
thus r > 0 by A4, XREAL_1:217; :: thesis: [.x0,(x0 + r).] c= dom f
A8: x0 in ].(x0 - g1),(x0 + g1).[ by A4, RCOMP_1:37;
abs ((x0 + (g1 / 2)) - x0) = g1 / 2 by A5, ABSVALUE:def 1;
then x0 + r in ].(x0 - g1),(x0 + g1).[ by A6, RCOMP_1:8;
then [.x0,(x0 + r).] c= ].(x0 - g1),(x0 + g1).[ by A8, XXREAL_2:def 12;
hence [.x0,(x0 + r).] c= dom f by A3, A4, XBOOLE_1:1; :: thesis: verum

end;

A9: for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n > 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = diff f,x0 ) by A1, A2, FDIFF_2:12;
A10: ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f )

proof

take r = g1 / 2; :: thesis: ( 0 < r & [.(x0 - r),x0.] c= dom f )
thus r > 0 by A4, XREAL_1:217; :: thesis: [.(x0 - r),x0.] c= dom f
A11: x0 in ].(x0 - g1),(x0 + g1).[ by A4, RCOMP_1:37;
abs ((x0 - (g1 / 2)) - x0) = abs ((- (g1 / 2)) + 0 )
.= abs (g1 / 2) by COMPLEX1:138
.= g1 / 2 by A5, ABSVALUE:def 1 ;
then x0 - r in ].(x0 - g1),(x0 + g1).[ by A6, RCOMP_1:8;
then [.(x0 - r),x0.] c= ].(x0 - g1),(x0 + g1).[ by A11, XXREAL_2:def 12;
hence [.(x0 - r),x0.] c= dom f by A3, A4, XBOOLE_1:1; :: thesis: verum

end;

for h being convergent_to_0 Real_Sequence
for c being V6 Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = diff f,x0 ) by A1, A2, FDIFF_2:12;
hence ( f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & diff f,x0 = Rdiff f,x0 & diff f,x0 = Ldiff f,x0 ) by A7, A9, A10, Th9, Th15; :: thesis: verum