theorem :: LIMFUNC2:21

for r, x0 being Real
for f being PartFunc of REAL,REAL holds
( ( f is_left_divergent_to+infty_in x0 & r > 0 implies r (#) f is_left_divergent_to+infty_in x0 ) & ( f is_left_divergent_to+infty_in x0 & r < 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r > 0 implies r (#) f is_left_divergent_to-infty_in x0 ) & ( f is_left_divergent_to-infty_in x0 & r < 0 implies r (#) f is_left_divergent_to+infty_in x0 ) )