let r, x0 be Real; :: thesis:
let f be PartFunc of REAL,REAL; :: thesis:
A1: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
thus ( f is_left_divergent_to+infty_in x0 & r > 0 implies r (#) f is_left_divergent_to+infty_in x0 ) :: thesis:

assume that
A2: f is_left_divergent_to+infty_in x0 and
A3: r > 0 ; :: thesis:
thus for r1 being Real st r1 < x0 holds
ex g being Real st
( r1 < g & g < x0 & g in dom (r (#) f) ) :: according to LIMFUNC2:def 2 :: thesis:

let r1 be Real; :: thesis:
assume r1 < x0 ; :: thesis:
then consider g being Real such that
A4: r1 < g and
A5: g < x0 and
A6: g in dom f by A2;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A4, A5, A6, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume that
A7: seq is convergent and
A8: lim seq = x0 and
A9: rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ; :: thesis:
A10: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
A11: rng seq c= (dom f) /\ (left_open_halfline x0) by A9, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A2, A7, A8;
then r (#) (f /* seq) is divergent_to+infty by A3, LIMFUNC1:13;
hence (r (#) f) /* seq is divergent_to+infty by A11, A10, RFUNCT_2:9, XBOOLE_1:1; :: thesis:

end;

thus ( f is_left_divergent_to+infty_in x0 & r < 0 implies r (#) f is_left_divergent_to-infty_in x0 ) :: thesis:

assume that
A12: f is_left_divergent_to+infty_in x0 and
A13: r < 0 ; :: thesis:
thus for r1 being Real st r1 < x0 holds
ex g being Real st
( r1 < g & g < x0 & g in dom (r (#) f) ) :: according to LIMFUNC2:def 3 :: thesis:

let r1 be Real; :: thesis:
assume r1 < x0 ; :: thesis:
then consider g being Real such that
A14: r1 < g and
A15: g < x0 and
A16: g in dom f by A12;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A14, A15, A16, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume that
A17: seq is convergent and
A18: lim seq = x0 and
A19: rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ; :: thesis:
A20: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
A21: rng seq c= (dom f) /\ (left_open_halfline x0) by A19, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A12, A17, A18;
then r (#) (f /* seq) is divergent_to-infty by A13, LIMFUNC1:13;
hence (r (#) f) /* seq is divergent_to-infty by A21, A20, RFUNCT_2:9, XBOOLE_1:1; :: thesis:

end;

thus ( f is_left_divergent_to-infty_in x0 & r > 0 implies r (#) f is_left_divergent_to-infty_in x0 ) :: thesis:

assume that
A22: f is_left_divergent_to-infty_in x0 and
A23: r > 0 ; :: thesis:
thus for r1 being Real st r1 < x0 holds
ex g being Real st
( r1 < g & g < x0 & g in dom (r (#) f) ) :: according to LIMFUNC2:def 3 :: thesis:

let r1 be Real; :: thesis:
assume r1 < x0 ; :: thesis:
then consider g being Real such that
A24: r1 < g and
A25: g < x0 and
A26: g in dom f by A22;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A24, A25, A26, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume that
A27: seq is convergent and
A28: lim seq = x0 and
A29: rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ; :: thesis:
A30: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
A31: rng seq c= (dom f) /\ (left_open_halfline x0) by A29, VALUED_1:def 5;
then f /* seq is divergent_to-infty by A22, A27, A28;
then r (#) (f /* seq) is divergent_to-infty by A23, LIMFUNC1:14;
hence (r (#) f) /* seq is divergent_to-infty by A31, A30, RFUNCT_2:9, XBOOLE_1:1; :: thesis:

end;

assume that
A32: f is_left_divergent_to-infty_in x0 and
A33: r < 0 ; :: thesis:
thus for r1 being Real st r1 < x0 holds
ex g being Real st
( r1 < g & g < x0 & g in dom (r (#) f) ) :: according to LIMFUNC2:def 2 :: thesis:

let r1 be Real; :: thesis:
assume r1 < x0 ; :: thesis:
then consider g being Real such that
A34: r1 < g and
A35: g < x0 and
A36: g in dom f by A32;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A34, A35, A36, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume that
A37: seq is convergent and
A38: lim seq = x0 and
A39: rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ; :: thesis:
A40: rng seq c= (dom f) /\ (left_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; :: thesis: