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 A1: ( f is_right_differentiable_in x0 & f . x0 <> 0 ) ; :: thesis: ( f ^ is_right_differentiable_in x0 & Rdiff (f ^ ),x0 = - ((Rdiff f,x0) / ((f . x0) ^2 )) )
then A2: f is_Rcontinuous_in x0 by Th7;
ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f ) by A1, Def3;
then consider r1 being Real such that
A3: ( r1 > 0 & [.x0,(x0 + r1).] c= dom f & ( for g being Real st g in [.x0,(x0 + r1).] holds
f . g <> 0 ) ) by A1, A2, Th8;

now

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 ( g in dom f & g in [.x0,(x0 + r1).] ) ; :: thesis: f . g <> 0
hence f . g <> 0 by A3; :: thesis: verum

end;

hence ( f ^ is_right_differentiable_in x0 & Rdiff (f ^ ),x0 = - ((Rdiff f,x0) / ((f . x0) ^2 )) ) by A1, Lm4; :: thesis: verum