let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_right_differentiable_in x0 holds
( 0 (#) f is_right_differentiable_in x0 & Rdiff ((0 (#) f),x0) = 0 )
let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 implies ( 0 (#) f is_right_differentiable_in x0 & Rdiff ((0 (#) f),x0) = 0 ) )
assume f is_right_differentiable_in x0 ; :: thesis: ( 0 (#) f is_right_differentiable_in x0 & Rdiff ((0 (#) f),x0) = 0 )
then consider e being Real such that
A1: ( e > 0 & [.x0,(x0 + e).] c= dom f ) by FDIFF_3:def 3;
A2: x0 < x0 + e by A1, XREAL_1:29;
then A3: x0 in [.x0,(x0 + e).] by XXREAL_1:1;
reconsider I = [.x0,(x0 + e).] as non empty closed_interval Subset of REAL by A2, XXREAL_1:1, MEASURE5:def 3;
A4: ( inf I = x0 & sup I = x0 + e ) by A2, XXREAL_2:25, XXREAL_2:29;

now :: thesis: for r being Real st r in rng (0 (#) f) holds
r in {0}

let r be Real; :: thesis: ( r in rng (0 (#) f) implies r in {0} )
assume r in rng (0 (#) f) ; :: thesis: r in {0}
then consider x being Element of REAL such that
A5: ( x in dom (0 (#) f) & r = (0 (#) f) . x ) by PARTFUN1:3;
(0 (#) f) . x = 0 * (f . x) by A5, VALUED_1:def 5;
hence r in {0} by A5, TARSKI:def 1; :: thesis: verum

end;

then A6: rng (0 (#) f) c= {0} ;
A7: I c= dom (0 (#) f) by A1, VALUED_1:def 5;
then dom (0 (#) f) <> {} ;
then A8: rng (0 (#) f) = {0} by A6, RELAT_1:42, ZFMISC_1:33;
then A9: 0 (#) f is_differentiable_on_interval I by A7, A2, A4, Th15;
hence 0 (#) f is_right_differentiable_in x0 by A4, XXREAL_1:1, Lm5; :: thesis: Rdiff ((0 (#) f),x0) = 0
A10: for x being Real st x in I holds
((0 (#) f) `\ I) . x = 0 by A2, A4, A8, A7, Th15;
((0 (#) f) `\ I) . x0 = Rdiff ((0 (#) f),x0) by A3, A4, A9, Def2;
hence Rdiff ((0 (#) f),x0) = 0 by A10, A2, XXREAL_1:1; :: thesis: verum