let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_differentiable_in x0 holds
( 0 (#) f is_left_differentiable_in x0 & Ldiff ((0 (#) f),x0) = 0 )
let x0 be Real; :: thesis: ( f is_left_differentiable_in x0 implies ( 0 (#) f is_left_differentiable_in x0 & Ldiff ((0 (#) f),x0) = 0 ) )
assume f is_left_differentiable_in x0 ; :: thesis: ( 0 (#) f is_left_differentiable_in x0 & Ldiff ((0 (#) f),x0) = 0 )
then consider e being Real such that
A1: ( e > 0 & [.(x0 - e),x0.] c= dom f ) by FDIFF_3:def 4;
A2: x0 - e < x0 by A1, XREAL_1:44;
then A3: x0 in [.(x0 - e),x0.] by XXREAL_1:1;
reconsider I = [.(x0 - e),x0.] as non empty closed_interval Subset of REAL by A2, XXREAL_1:1, MEASURE5:def 3;
A4: ( inf I = x0 - e & sup I = x0 ) 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, ZFMISC_1:33, RELAT_1:42;
then A9: 0 (#) f is_differentiable_on_interval I by A7, A2, A4, Th15;
hence 0 (#) f is_left_differentiable_in x0 by A4, XXREAL_1:1, Lm6; :: thesis: Ldiff ((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 = Ldiff ((0 (#) f),x0) by A3, A4, A9, Def2;
hence Ldiff ((0 (#) f),x0) = 0 by A10, A2, XXREAL_1:1; :: thesis: verum