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 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))) = 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 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))) = 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 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))) = g ) ) ) ) by Def5; :: thesis: ( ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( 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))) = 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 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))) = g ) ) implies ( f is_left_differentiable_in x0 & Ldiff (f,x0) = g ) ) :: thesis: verum

( 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 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))) = 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 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))) = 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 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))) = g ) ) ) ) by Def5; :: thesis: ( ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) & ( 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))) = 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 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))) = g ) ) implies ( f is_left_differentiable_in x0 & Ldiff (f,x0) = g ) ) :: thesis: verum

proof

assume that

A1: ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) and

A2: 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))) = g ) ; :: thesis: ( f is_left_differentiable_in x0 & Ldiff (f,x0) = g )

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 by A2;

hence A3: f is_left_differentiable_in x0 by A1; :: thesis: Ldiff (f,x0) = g

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

lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g by A2;

hence Ldiff (f,x0) = g by A3, Def5; :: thesis: verum

end;A1: ex r being Real st

( 0 < r & [.(x0 - r),x0.] c= dom f ) and

A2: 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))) = g ) ; :: thesis: ( f is_left_differentiable_in x0 & Ldiff (f,x0) = g )

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 by A2;

hence A3: f is_left_differentiable_in x0 by A1; :: thesis: Ldiff (f,x0) = g

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

lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = g by A2;

hence Ldiff (f,x0) = g by A3, Def5; :: thesis: verum