let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.[ c= dom f & f | [.a,b.[ is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_right_convergent_in a holds
( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) )
let a, b be Real; :: thesis: ( a < b & [.a,b.[ c= dom f & f | [.a,b.[ is continuous & f is_differentiable_on ].a,b.[ & f `| ].a,b.[ is_right_convergent_in a implies ( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) ) )
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: f | [.a,b.[ is continuous and
A4: f is_differentiable_on ].a,b.[ and
A5: f `| ].a,b.[ is_right_convergent_in a ; :: thesis: ( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) )
consider e being Real such that
A6: ( a < e & e < b ) by A1, XREAL_1:5;
[.a,e.] c= [.a,b.[ by A6, XXREAL_1:43;
then A7: [.a,e.] c= dom f by A2;
set r = e - a;
a + (e - a) = e ;
then A8: ex r being Real st
( r > 0 & [.a,(a + r).] c= dom f ) by A7, A6, XREAL_1:50;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {a} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {a} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a) )
let c be constant Real_Sequence; :: thesis: ( rng c = {a} & rng (h + c) c= dom f & ( for n being Nat holds h . n > 0 ) implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a) ) )
assume that
A9: rng c = {a} and
A10: rng (h + c) c= dom f and
A11: for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a) )
A12: ( h is convergent & lim h = 0 ) ;
A13: a in [.a,b.[ by A1, XXREAL_1:3;
A14: dom (f `| ].a,b.[) = ].a,b.[ by A4, FDIFF_1:def 7;
A15: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p

proof

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p
then consider R being Real such that
A16: a < R and
A17: for r1 being Real st r1 < R & a < r1 & r1 in dom (f `| ].a,b.[) holds
|.(((f `| ].a,b.[) . r1) - (lim_right ((f `| ].a,b.[),a))).| < p by A5, LIMFUNC2:42;
set r = min (b,R);
A18: ( a < min (b,R) & min (b,R) <= b & min (b,R) <= R ) by A1, A16, XXREAL_0:17, XXREAL_0:21;
then (min (b,R)) - a > 0 by XREAL_1:50;
then consider N being Nat such that
A19: for m being Nat st N <= m holds
|.((h . m) - 0).| < (min (b,R)) - a by A12, SEQ_2:def 7;
take N ; :: thesis: for m being Nat st N <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p
thus for m being Nat st N <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p :: thesis: verum

proof

let m be Nat; :: thesis: ( N <= m implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p )
assume N <= m ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p
then ( h . m > 0 & |.((h . m) - 0).| < (min (b,R)) - a ) by A11, A19;
then A20: h . m < (min (b,R)) - a by ABSVALUE:def 1;
A21: m in NAT by ORDINAL1:def 12;
then A22: ( m in dom (h + c) & m in dom c ) by FUNCT_2:def 1;
then c . m in rng c by FUNCT_1:3;
then A23: c . m = a by A9, TARSKI:def 1;
then A24: (h + c) . m = (h . m) + a by A22, VALUED_1:def 1;
then A25: (h + c) . m < ((min (b,R)) - a) + a by A20, XREAL_1:8;
set H = (h + c) . m;
A26: a < (h + c) . m by A11, A24, XREAL_1:29;
A27: (h + c) . m < b by A18, A25, XXREAL_0:2;
then [.a,((h + c) . m).] c= [.a,b.[ by XXREAL_1:43;
then A28: [.a,((h + c) . m).] c= dom f by A2;
A29: f | [.a,((h + c) . m).] is continuous by A3, A27, FCONT_1:16, XXREAL_1:43;
A30: ].a,((h + c) . m).[ c= ].a,b.[ by A27, XXREAL_1:46;
then consider x0 being Real such that
A31: x0 in ].a,((h + c) . m).[ and
A32: diff (f,x0) = ((f . ((h + c) . m)) - (f . a)) / (((h + c) . m) - a) by A26, A28, A29, A4, FDIFF_1:26, ROLLE:3;
A33: ( a < x0 & x0 < (h + c) . m ) by A31, XXREAL_1:4;
then x0 < min (b,R) by A25, XXREAL_0:2;
then A34: x0 < R by A18, XXREAL_0:2;
A35: dom ((f /* (h + c)) - (f /* c)) = NAT /\ NAT by FUNCT_2:def 1;
( f . ((h + c) . m) = (f /* (h + c)) . m & f . a = (f /* c) . m ) by A10, A21, A23, A13, A2, A9, ZFMISC_1:31, FUNCT_2:108;
then (f . ((h + c) . m)) - (f . a) = ((f /* (h + c)) - (f /* c)) . m by A35, VALUED_1:13, ORDINAL1:def 12;
then (((f /* (h + c)) - (f /* c)) /" h) . m = ((f . ((h + c) . m)) - (f . a)) / (((h + c) . m) - a) by A24, VALUED_1:17;
then ((h ") (#) ((f /* (h + c)) - (f /* c))) . m = (f `| ].a,b.[) . x0 by A4, A30, A31, A32, FDIFF_1:def 7;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - (lim_right ((f `| ].a,b.[),a))).| < p by A17, A33, A34, A30, A31, A14; :: thesis: verum

end;

end;

hence (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a)
hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = lim_right ((f `| ].a,b.[),a) by A15, SEQ_2:def 7; :: thesis: verum

end;

hence ( f is_right_differentiable_in a & Rdiff (f,a) = lim_right ((f `| ].a,b.[),a) ) by A8, FDIFF_3:15; :: thesis: verum