for b₁ being PartFunc of REAL , REAL
for b₂ being Real st b₁ is_continuous_in b₂ & ( for b₃, b₄ being Real st b₃ < b₂ & b₂ < b₄ holds
ex b₅, b₆ being Real st
( b₃ < b₅ & b₅ < b₂ & b₅ in dom b₁ & b₆ < b₄ & b₂ < b₆ & b₆ in dom b₁ ) ) holds
b₁ is_convergent_in b₂

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real holds
( b₁ is_right_convergent_in b₂ & lim_right b₁,b₂ = b₃ iff ( ( for b₄ being Real st b₂ < b₄ holds
ex b₅ being Real st
( b₅ < b₄ & b₂ < b₅ & b₅ in dom b₁ ) ) & ( for b₄ being Real_Sequence st b₄ is convergent & lim b₄ = b₂ & rng b₄ c= (dom b₁) /\ (right_open_halfline b₂) holds
( b₁ * b₄ is convergent & lim (b₁ * b₄) = b₃ ) ) ) )

for b₁ being PartFunc of REAL , REAL
for b₂, b₃ being Real holds
( b₁ is_left_convergent_in b₂ & lim_left b₁,b₂ = b₃ iff ( ( for b₄ being Real st b₄ < b₂ holds
ex b₅ being Real st
( b₄ < b₅ & b₅ < b₂ & b₅ in dom b₁ ) ) & ( for b₄ being Real_Sequence st b₄ is convergent & lim b₄ = b₂ & rng b₄ c= (dom b₁) /\ (left_open_halfline b₂) holds
( b₁ * b₄ is convergent & lim (b₁ * b₄) = b₃ ) ) ) )

for b₁ being PartFunc of REAL , REAL
for b₂ being Real st ex b₃ being Neighbourhood of b₂ st b₃ \ {b₂} c= dom b₁ holds
for b₃, b₄ being Real st b₃ < b₂ & b₂ < b₄ holds
ex b₅, b₆ being Real st
( b₃ < b₅ & b₅ < b₂ & b₅ in dom b₁ & b₆ < b₄ & b₂ < b₆ & b₆ in dom b₁ )

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Neighbourhood of b₃ st
( b₁ is_differentiable_on b₄ & b₂ is_differentiable_on b₄ & b₄ \ {b₃} c= dom (b₁ / b₂) & b₄ c= dom ((b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & (b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄) is_divergent_to+infty_in b₃ ) holds
b₁ / b₂ is_divergent_to+infty_in b₃

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Neighbourhood of b₃ st
( b₁ is_differentiable_on b₄ & b₂ is_differentiable_on b₄ & b₄ \ {b₃} c= dom (b₁ / b₂) & b₄ c= dom ((b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & (b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄) is_divergent_to-infty_in b₃ ) holds
b₁ / b₂ is_divergent_to-infty_in b₃

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Real st
( b₄ > 0 & b₁ is_differentiable_on ].b₃,(b₃ + b₄).[ & b₂ is_differentiable_on ].b₃,(b₃ + b₄).[ & ].b₃,(b₃ + b₄).[ c= dom (b₁ / b₂) & [.b₃,(b₃ + b₄).] c= dom ((b₁ `| ].b<sub>3</sub>,(b<sub>3</sub> + b<sub>4</sub>).[) / (b<sub>2</sub> `| ].b₃,(b₃ + b₄).[)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & b₁ is_continuous_in b₃ & b₂ is_continuous_in b₃ & (b₁ `| ].b<sub>3</sub>,(b<sub>3</sub> + b<sub>4</sub>).[) / (b<sub>2</sub> `| ].b₃,(b₃ + b₄).[) is_right_convergent_in b₃ ) holds
( b₁ / b₂ is_right_convergent_in b₃ & ex b₄ being Real st
( b₄ > 0 & lim_right (b₁ / b₂),b₃ = lim_right ((b₁ `| ].b<sub>3</sub>,(b<sub>3</sub> + b<sub>4</sub>).[) / (b<sub>2</sub> `| ].b₃,(b₃ + b₄).[)),b₃ ) )

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Real st
( b₄ > 0 & b₁ is_differentiable_on ].(b₃ - b₄),b₃.[ & b₂ is_differentiable_on ].(b₃ - b₄),b₃.[ & ].(b₃ - b₄),b₃.[ c= dom (b₁ / b₂) & [.(b₃ - b₄),b₃.] c= dom ((b₁ `| ].(b<sub>3</sub> - b<sub>4</sub>),b<sub>3</sub>.[) / (b<sub>2</sub> `| ].(b₃ - b₄),b₃.[)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & b₁ is_continuous_in b₃ & b₂ is_continuous_in b₃ & (b₁ `| ].(b<sub>3</sub> - b<sub>4</sub>),b<sub>3</sub>.[) / (b<sub>2</sub> `| ].(b₃ - b₄),b₃.[) is_left_convergent_in b₃ ) holds
( b₁ / b₂ is_left_convergent_in b₃ & ex b₄ being Real st
( b₄ > 0 & lim_left (b₁ / b₂),b₃ = lim_left ((b₁ `| ].(b<sub>3</sub> - b<sub>4</sub>),b<sub>3</sub>.[) / (b<sub>2</sub> `| ].(b₃ - b₄),b₃.[)),b₃ ) )

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Neighbourhood of b₃ st
( b₁ is_differentiable_on b₄ & b₂ is_differentiable_on b₄ & b₄ \ {b₃} c= dom (b₁ / b₂) & b₄ c= dom ((b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & (b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄) is_convergent_in b₃ ) holds
( b₁ / b₂ is_convergent_in b₃ & ex b₄ being Neighbourhood of b₃ st lim (b₁ / b₂),b₃ = lim ((b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄)),b₃ )

for b₁, b₂ being PartFunc of REAL , REAL
for b₃ being Real st ex b₄ being Neighbourhood of b₃ st
( b₁ is_differentiable_on b₄ & b₂ is_differentiable_on b₄ & b₄ \ {b₃} c= dom (b₁ / b₂) & b₄ c= dom ((b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄)) & b₁ . b₃ = 0 & b₂ . b₃ = 0 & (b₁ `| b<sub>4</sub>) / (b<sub>2</sub> `| b₄) is_continuous_in b₃ ) holds
( b₁ / b₂ is_convergent_in b₃ & lim (b₁ / b₂),b₃ = (diff b₁,b₃) / (diff b₂,b₃) )