let f be PartFunc of REAL ,REAL ; :: thesis: for x0, g being Real holds
( f is_left_differentiable_in x0 & Ldiff f,x0 = g iff ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) ) )
let x0, g be Real; :: thesis: ( f is_left_differentiable_in x0 & Ldiff f,x0 = g iff ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) ) )
thus ( f is_left_differentiable_in x0 & Ldiff f,x0 = g implies ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) ) ) by Def4, Def5; :: thesis: ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) implies ( f is_left_differentiable_in x0 & Ldiff f,x0 = g ) )
thus ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) implies ( f is_left_differentiable_in x0 & Ldiff f,x0 = g ) ) :: thesis: verum

proof

assume A1: ( ex r being Real st
( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( for h being convergent_to_0 Real_Sequence
for c being V8() 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))) = g ) ) ) ; :: thesis: ( f is_left_differentiable_in x0 & Ldiff f,x0 = g )
then for h being convergent_to_0 Real_Sequence
for c being V8() 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 ;
hence A2: f is_left_differentiable_in x0 by A1, Def4; :: thesis: Ldiff f,x0 = g
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & ( for n being Element of NAT holds h . n < 0 ) holds
lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) = g by A1;
hence Ldiff f,x0 = g by A2, Def5; :: thesis: verum

end;