for f, g being PartFunc of REAL,REAL
for x0 being Real st ex N being Neighbourhood of x0 st
( N c= dom f & N c= dom g & 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