assume that
A1: seq is divergent_to-infty and
A2: r > 0 ; :: thesis:
let g be Real; :: according to LIMFUNC1:def 5 :: thesis:
consider n being Nat such that
A3: for m being Nat st n <= m holds
seq . m < g / r by A1;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then seq . m < g / r by A3;
then r * (seq . m) < (g / r) * r by A2, XREAL_1:68;
then r * (seq . m) < g by A2, XCMPLX_1:87;
hence (r (#) seq) . m < g by SEQ_1:9; :: thesis:

end;

assume that
A4: seq is divergent_to-infty and
A5: r < 0 ; :: thesis:
let g be Real; :: according to LIMFUNC1:def 4 :: thesis:
consider n being Nat such that
A6: for m being Nat st n <= m holds
seq . m < g / r by A4;
take n ; :: thesis:
let m be Nat; :: thesis:
assume n <= m ; :: thesis:
then seq . m < g / r by A6;
then (g / r) * r < r * (seq . m) by A5, XREAL_1:69;
then g < r * (seq . m) by A5, XCMPLX_1:87;
hence g < (r (#) seq) . m by SEQ_1:9; :: thesis:

end;

let x be Real; :: according to MEMBERED:def 15 :: thesis:
thus ( x in rng (r (#) seq) implies x in {0} ) :: thesis:

assume x in rng (r (#) seq) ; :: thesis:
then consider n being Element of NAT such that
A8: x = (r (#) seq) . n by FUNCT_2:113;
x = r * (seq . n) by A8, SEQ_1:9
.= 0 by A7 ;
hence x in {0} by TARSKI:def 1; :: thesis:

end;

assume x in {0} ; :: thesis:
then A9: x = 0 by TARSKI:def 1;
(r (#) seq) . 0 = r * (seq . 0) by SEQ_1:9
.= 0 by A7 ;
hence x in rng (r (#) seq) by A9, VALUED_0:28; :: thesis:

end;