let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f is_right_differentiable_in x0 & f . x0 <> 0 holds
( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
let x0 be Real; :: thesis: ( f is_right_differentiable_in x0 & f . x0 <> 0 implies ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) )
assume that
A1: f is_right_differentiable_in x0 and
A2: f . x0 <> 0 ; :: thesis: ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) )
consider r1 being Real such that
A3: r1 > 0 and
[.x0,(x0 + r1).] c= dom f and
A4: for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> 0 by A1, A2, Th7, Th8;
now :: thesis: ex r1 being Real st
( r1 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r1).] holds
f . g <> 0 ) )
take r1 = r1; :: thesis: ( r1 > 0 & ( for g being Real st g in dom f & g in [.x0,(x0 + r1).] holds
f . g <> 0 ) )
thus r1 > 0 by A3; :: thesis: for g being Real st g in dom f & g in [.x0,(x0 + r1).] holds
f . g <> 0
let g be Real; :: thesis: ( g in dom f & g in [.x0,(x0 + r1).] implies f . g <> 0 )
assume that
g in dom f and
A5: g in [.x0,(x0 + r1).] ; :: thesis: f . g <> 0
thus f . g <> 0 by A4, A5; :: thesis: verum
end;
hence ( f ^ is_right_differentiable_in x0 & Rdiff ((f ^),x0) = - ((Rdiff (f,x0)) / ((f . x0) ^2)) ) by A1, Lm4; :: thesis: verum