theorem :: L_HOSPIT:8

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 - r),x0.] c= dom f & [.(x0 - r),x0.] c= dom g & f is_differentiable_on ].(x0 - r),x0.[ & g is_differentiable_on ].(x0 - r),x0.[ & ].(x0 - r),x0.[ c= dom (f / g) & [.(x0 - r),x0.] c= dom ((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[) is_left_convergent_in x0 ) holds
( f / g is_left_convergent_in x0 & ex r being Real st
( r > 0 & lim_left ((f / g),x0) = lim_left (((f `| ].(x0 - r),x0.[) / (g `| ].(x0 - r),x0.[)),x0) ) )