theorem :: L_HOSPIT:7

for f, g being PartFunc of REAL,REAL
for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds
( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) )