for f being PartFunc of REAL , REAL
for x0 being Real st f is_continuous_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) holds
f is_convergent_in x0

for f being PartFunc of REAL , REAL
for x0, t being Real holds
( f is_right_convergent_in x0 & lim_right f,x0 = t iff ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f * a is convergent & lim (f * a) = t ) ) ) )

for f being PartFunc of REAL , REAL
for x0, t being Real holds
( f is_left_convergent_in x0 & lim_left f,x0 = t iff ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f * a is convergent & lim (f * a) = t ) ) ) )

for f being PartFunc of REAL , REAL
for x0 being Real st ex N being Neighbourhood of x0 st N \ {x0} c= dom f holds
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_divergent_to+infty_in x0 ) holds
f / g is_divergent_to+infty_in x0

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_divergent_to-infty_in x0 ) holds
f / g is_divergent_to-infty_in x0

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex r being Real st
( r > 0 & 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 ) )

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex r being Real st
( r > 0 & 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 ) )

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_convergent_in x0 ) holds
( f / g is_convergent_in x0 & ex N being Neighbourhood of x0 st lim (f / g),x0 = lim ((f `| N) / (g `| N)),x0 )

for f, g being PartFunc of REAL , REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( f is_differentiable_on N & g is_differentiable_on N & N \ {x0} c= dom (f / g) & N c= dom ((f `| N) / (g `| N)) & f . x0 = 0 & g . x0 = 0 & (f `| N) / (g `| N) is_continuous_in x0 ) holds
( f / g is_convergent_in x0 & lim (f / g),x0 = (diff f,x0) / (diff g,x0) )