let f be PartFunc of REAL,REAL; :: thesis:
let r be Real; :: thesis:
thus ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) :: thesis:

assume that
A1: f is divergent_in+infty_to+infty and
A2: r > 0 ; :: thesis:

A3: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A4: seq is divergent_to+infty and
A5: rng seq c= dom (r (#) f) ; :: thesis:
A6: rng seq c= dom f by A5, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A1, A4;
then r (#) (f /* seq) is divergent_to+infty by A2, Th13;
hence (r (#) f) /* seq is divergent_to+infty by A6, RFUNCT_2:9; :: thesis:

end;

let r1 be Real; :: thesis:
consider g being Real such that
A7: ( r1 < g & g in dom f ) by A1;
take g = g; :: thesis:
thus ( r1 < g & g in dom (r (#) f) ) by A7, VALUED_1:def 5; :: thesis:

end;

hence r (#) f is divergent_in+infty_to+infty by A3; :: thesis:

end;

thus ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) :: thesis:

assume that
A8: f is divergent_in+infty_to+infty and
A9: r < 0 ; :: thesis:

A10: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A11: seq is divergent_to+infty and
A12: rng seq c= dom (r (#) f) ; :: thesis:
A13: rng seq c= dom f by A12, VALUED_1:def 5;
then f /* seq is divergent_to+infty by A8, A11;
then r (#) (f /* seq) is divergent_to-infty by A9, Th13;
hence (r (#) f) /* seq is divergent_to-infty by A13, RFUNCT_2:9; :: thesis:

end;

let r1 be Real; :: thesis:
consider g being Real such that
A14: ( r1 < g & g in dom f ) by A8;
take g = g; :: thesis:
thus ( r1 < g & g in dom (r (#) f) ) by A14, VALUED_1:def 5; :: thesis:

end;

hence r (#) f is divergent_in+infty_to-infty by A10; :: thesis:

end;

thus ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) :: thesis:

assume that
A15: f is divergent_in+infty_to-infty and
A16: r > 0 ; :: thesis:

A17: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A18: seq is divergent_to+infty and
A19: rng seq c= dom (r (#) f) ; :: thesis:
A20: rng seq c= dom f by A19, VALUED_1:def 5;
then f /* seq is divergent_to-infty by A15, A18;
then r (#) (f /* seq) is divergent_to-infty by A16, Th14;
hence (r (#) f) /* seq is divergent_to-infty by A20, RFUNCT_2:9; :: thesis:

end;

let r1 be Real; :: thesis:
consider g being Real such that
A21: ( r1 < g & g in dom f ) by A15;
take g = g; :: thesis:
thus ( r1 < g & g in dom (r (#) f) ) by A21, VALUED_1:def 5; :: thesis:

end;

hence r (#) f is divergent_in+infty_to-infty by A17; :: thesis:

end;

assume that
A22: f is divergent_in+infty_to-infty and
A23: r < 0 ; :: thesis:

A24: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A25: seq is divergent_to+infty and
A26: rng seq c= dom (r (#) f) ; :: thesis:
A27: rng seq c= dom f by A26, VALUED_1:def 5;
then f /* seq is divergent_to-infty by A22, A25;
then r (#) (f /* seq) is divergent_to+infty by A23, Th14;
hence (r (#) f) /* seq is divergent_to+infty by A27, RFUNCT_2:9; :: thesis:

end;

let r1 be Real; :: thesis:
consider g being Real such that
A28: ( r1 < g & g in dom f ) by A22;
take g = g; :: thesis:
thus ( r1 < g & g in dom (r (#) f) ) by A28, VALUED_1:def 5; :: thesis:

end;

hence r (#) f is divergent_in+infty_to+infty by A24; :: thesis: