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

now :: thesis: ex r1 being Real st
( r1 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r1).] holds
f2 . g <> 0 ) )

take r1 = r1; :: thesis: ( r1 > 0 & ( for g being Real st g in dom f2 & g in [.x0,(x0 + r1).] holds
f2 . g <> 0 ) )
thus r1 > 0 by A4; :: thesis: for g being Real st g in dom f2 & g in [.x0,(x0 + r1).] holds
f2 . g <> 0
let g be Real; :: thesis: ( g in dom f2 & g in [.x0,(x0 + r1).] implies f2 . g <> 0 )
assume that
g in dom f2 and
A6: g in [.x0,(x0 + r1).] ; :: thesis: f2 . g <> 0
thus f2 . g <> 0 by A5, A6; :: thesis: verum

end;

hence ( f1 / f2 is_right_differentiable_in x0 & Rdiff ((f1 / f2),x0) = (((Rdiff (f1,x0)) * (f2 . x0)) - ((Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2) ) by A1, A2, Lm3; :: thesis: verum