let f be PartFunc of REAL,REAL; :: thesis: for x0, r being Real st f is_right_differentiable_in x0 & rng f = {r} holds
Rdiff (f,x0) = 0
let x0, r be Real; :: thesis: ( f is_right_differentiable_in x0 & rng f = {r} implies Rdiff (f,x0) = 0 )
assume that
A1: f is_right_differentiable_in x0 and
A2: rng f = {r} ; :: thesis: Rdiff (f,x0) = 0
A3: ex e being Real st
( e > 0 & [.x0,(x0 + e).] c= dom f ) by A1, FDIFF_3:def 3;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & 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))) = 0 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & 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))) = 0 )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & 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))) = 0 ) )
assume that
A4: rng c = {x0} and
A5: rng (h + c) c= dom f and
A6: for n being Nat holds h . n > 0 ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 )
thus A7: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A4, A5, A6, FDIFF_3:def 3; :: thesis: lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0
consider e being Real such that
A8: ( e > 0 & [.x0,(x0 + e).] c= dom f ) by A1, FDIFF_3:def 3;
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) - 0).| < 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) - 0).| < p )
assume A9: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - 0).| < p
take n = 0 ; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - 0).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - 0).| < p )
assume n <= m ; :: thesis: |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - 0).| < p
x0 < x0 + e by A8, XREAL_1:29;
then A10: x0 in [.x0,(x0 + e).] by XXREAL_1:1;
then A11: rng c c= dom f by A8, A4, ZFMISC_1:31;
A12: ( f /* (h + c) = f * (h + c) & f /* c = f * c ) by A5, A8, A4, A10, ZFMISC_1:31, FUNCT_2:def 11;
A13: ( dom (h + c) = NAT & dom c = NAT ) by FUNCT_2:def 1;
then ( m in dom (h + c) & m in dom c ) by ORDINAL1:def 12;
then ( m in dom (f * (h + c)) & m in dom (f * c) ) by A5, A10, A8, A4, ZFMISC_1:31, RELAT_1:27;
then m in (dom (f * (h + c))) /\ (dom (f * c)) by XBOOLE_0:def 4;
then A14: m in dom ((f * (h + c)) - (f * c)) by VALUED_1:12;
( (h + c) . m in rng (h + c) & c . m in rng c ) by A13, ORDINAL1:def 12, FUNCT_1:3;
then ( f . ((h + c) . m) in rng f & f . (c . m) in rng f ) by A5, A11, FUNCT_1:3;
then ( f . ((h + c) . m) = r & f . (c . m) = r ) by A2, TARSKI:def 1;
then A15: ( (f * (h + c)) . m = r & (f * c) . m = r ) by A13, ORDINAL1:def 12, FUNCT_1:13;
((h ") (#) ((f /* (h + c)) - (f /* c))) . m = ((h ") . m) * (((f * (h + c)) - (f * c)) . m) by A12, VALUED_1:5
.= ((h ") . m) * (((f * (h + c)) . m) - ((f * c) . m)) by A14, VALUED_1:13 ;
hence |.((((h ") (#) ((f /* (h + c)) - (f /* c))) . m) - 0).| < p by A9, A15, COMPLEX1:44; :: thesis: verum

end;

end;

hence lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = 0 by A7, SEQ_2:def 7; :: thesis: verum

end;

hence Rdiff (f,x0) = 0 by A3, FDIFF_3:15; :: thesis: verum