let x0, r be Real; :: thesis:
let f be PartFunc of REAL ,REAL ; :: thesis:
thus ( f is_left_divergent_to+infty_in x0 & r > 0 implies r (#) f is_left_divergent_to+infty_in x0 ) :: thesis:

assume A1: ( f is_left_divergent_to+infty_in x0 & 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
A2: ( r1 < g & g < x0 & g in dom f ) by A1, Def2;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A2, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume A3: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ) ; :: thesis:
then A4: rng seq c= (dom f) /\ (left_open_halfline x0) by VALUED_1:def 5;
then f /* seq is divergent_to+infty by A1, A3, Def2;
then A5: r (#) (f /* seq) is divergent_to+infty by A1, LIMFUNC1:40;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
hence (r (#) f) /* seq is divergent_to+infty by A4, A5, RFUNCT_2:24, 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 A6: ( f is_left_divergent_to+infty_in x0 & 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
A7: ( r1 < g & g < x0 & g in dom f ) by A6, Def2;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A7, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume A8: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ) ; :: thesis:
then A9: rng seq c= (dom f) /\ (left_open_halfline x0) by VALUED_1:def 5;
then f /* seq is divergent_to+infty by A6, A8, Def2;
then A10: r (#) (f /* seq) is divergent_to-infty by A6, LIMFUNC1:40;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
hence (r (#) f) /* seq is divergent_to-infty by A9, A10, RFUNCT_2:24, 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 A11: ( f is_left_divergent_to-infty_in x0 & 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
A12: ( r1 < g & g < x0 & g in dom f ) by A11, Def3;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A12, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume A13: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ) ; :: thesis:
then A14: rng seq c= (dom f) /\ (left_open_halfline x0) by VALUED_1:def 5;
then f /* seq is divergent_to-infty by A11, A13, Def3;
then A15: r (#) (f /* seq) is divergent_to-infty by A11, LIMFUNC1:41;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
hence (r (#) f) /* seq is divergent_to-infty by A14, A15, RFUNCT_2:24, XBOOLE_1:1; :: thesis:

end;

assume A16: ( f is_left_divergent_to-infty_in x0 & 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
A17: ( r1 < g & g < x0 & g in dom f ) by A16, Def3;
take g ; :: thesis:
thus ( r1 < g & g < x0 & g in dom (r (#) f) ) by A17, VALUED_1:def 5; :: thesis:

end;

let seq be Real_Sequence; :: thesis:
assume A18: ( seq is convergent & lim seq = x0 & rng seq c= (dom (r (#) f)) /\ (left_open_halfline x0) ) ; :: thesis:
then A19: rng seq c= (dom f) /\ (left_open_halfline x0) by VALUED_1:def 5;
then f /* seq is divergent_to-infty by A16, A18, Def3;
then A20: r (#) (f /* seq) is divergent_to+infty by A16, LIMFUNC1:41;
(dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
hence (r (#) f) /* seq is divergent_to+infty by A19, A20, RFUNCT_2:24, XBOOLE_1:1; :: thesis: