let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_left_differentiable_in x0 & f . x0 <> 0 holds

( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

let x0 be Real; :: thesis: ( f is_left_differentiable_in x0 & f . x0 <> 0 implies ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) ) )

assume that

A1: f is_left_differentiable_in x0 and

A2: f . x0 <> 0 ; :: thesis: ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

consider r1 being Real such that

A3: r1 > 0 and

[.(x0 - r1),x0.] c= dom f and

A4: for g being Real st g in [.(x0 - r1),x0.] holds

f . g <> 0 by A1, A2, Th5, Th6;

( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

let x0 be Real; :: thesis: ( f is_left_differentiable_in x0 & f . x0 <> 0 implies ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) ) )

assume that

A1: f is_left_differentiable_in x0 and

A2: f . x0 <> 0 ; :: thesis: ( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )

consider r1 being Real such that

A3: r1 > 0 and

[.(x0 - r1),x0.] c= dom f and

A4: for g being Real st g in [.(x0 - r1),x0.] holds

f . g <> 0 by A1, A2, Th5, Th6;

now :: thesis: ex r1 being Real st

( r1 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r1),x0.] holds

f . g <> 0 ) )

hence
( f ^ is_left_differentiable_in x0 & Ldiff ((f ^),x0) = - ((Ldiff (f,x0)) / ((f . x0) ^2)) )
by A1, Lm2; :: thesis: verum( r1 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r1),x0.] holds

f . g <> 0 ) )

take r1 = r1; :: thesis: ( r1 > 0 & ( for g being Real st g in dom f & g in [.(x0 - r1),x0.] holds

f . g <> 0 ) )

thus r1 > 0 by A3; :: thesis: for g being Real st g in dom f & g in [.(x0 - r1),x0.] holds

f . g <> 0

let g be Real; :: thesis: ( g in dom f & g in [.(x0 - r1),x0.] implies f . g <> 0 )

assume that

g in dom f and

A5: g in [.(x0 - r1),x0.] ; :: thesis: f . g <> 0

thus f . g <> 0 by A4, A5; :: thesis: verum

end;f . g <> 0 ) )

thus r1 > 0 by A3; :: thesis: for g being Real st g in dom f & g in [.(x0 - r1),x0.] holds

f . g <> 0

let g be Real; :: thesis: ( g in dom f & g in [.(x0 - r1),x0.] implies f . g <> 0 )

assume that

g in dom f and

A5: g in [.(x0 - r1),x0.] ; :: thesis: f . g <> 0

thus f . g <> 0 by A4, A5; :: thesis: verum