let r, x0 be Real; for f being PartFunc of REAL,REAL holds
( ( f is_right_divergent_to+infty_in x0 & r > 0 implies r (#) f is_right_divergent_to+infty_in x0 ) & ( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )
let f be PartFunc of REAL,REAL; ( ( f is_right_divergent_to+infty_in x0 & r > 0 implies r (#) f is_right_divergent_to+infty_in x0 ) & ( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )
A1:
(dom f) /\ (right_open_halfline x0) c= dom f
by XBOOLE_1:17;
thus
( f is_right_divergent_to+infty_in x0 & r > 0 implies r (#) f is_right_divergent_to+infty_in x0 )
( ( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )
thus
( f is_right_divergent_to+infty_in x0 & r < 0 implies r (#) f is_right_divergent_to-infty_in x0 )
( ( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 ) & ( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 ) )
thus
( f is_right_divergent_to-infty_in x0 & r > 0 implies r (#) f is_right_divergent_to-infty_in x0 )
( f is_right_divergent_to-infty_in x0 & r < 0 implies r (#) f is_right_divergent_to+infty_in x0 )
assume that
A32:
f is_right_divergent_to-infty_in x0
and
A33:
r < 0
; r (#) f is_right_divergent_to+infty_in x0
thus
for r1 being Real st x0 < r1 holds
ex g being Real st
( g < r1 & x0 < g & g in dom (r (#) f) )
LIMFUNC2:def 5 for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (right_open_halfline x0) holds
(r (#) f) /* seq is divergent_to+infty
let seq be Real_Sequence; ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (right_open_halfline x0) implies (r (#) f) /* seq is divergent_to+infty )
assume that
A37:
seq is convergent
and
A38:
lim seq = x0
and
A39:
rng seq c= (dom (r (#) f)) /\ (right_open_halfline x0)
; (r (#) f) /* seq is divergent_to+infty
A40:
rng seq c= (dom f) /\ (right_open_halfline x0)
by A39, VALUED_1:def 5;
then
f /* seq is divergent_to-infty
by A32, A37, A38;
then
r (#) (f /* seq) is divergent_to+infty
by A33, LIMFUNC1:14;
hence
(r (#) f) /* seq is divergent_to+infty
by A40, A1, RFUNCT_2:9, XBOOLE_1:1; verum