let seq be Real_Sequence; :: thesis: for r being Real holds
( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )
let r be Real; :: thesis: ( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )
thus ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) :: thesis: ( ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) )

proof

assume that
A1: seq is divergent_to-infty and
A2: r > 0 ; :: thesis: r (#) seq is divergent_to-infty
let g be Real; :: according to LIMFUNC1:def 5 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(r (#) seq) . m < g
consider n being Nat such that
A3: for m being Nat st n <= m holds
seq . m < g / r by A1;
take n ; :: thesis: for m being Nat st n <= m holds
(r (#) seq) . m < g
let m be Nat; :: thesis: ( n <= m implies (r (#) seq) . m < g )
assume n <= m ; :: thesis: (r (#) seq) . m < g
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: verum

end;

thus ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) :: thesis: ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) )

proof

assume that
A4: seq is divergent_to-infty and
A5: r < 0 ; :: thesis: r (#) seq is divergent_to+infty
let g be Real; :: according to LIMFUNC1:def 4 :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g < (r (#) seq) . m
consider n being Nat such that
A6: for m being Nat st n <= m holds
seq . m < g / r by A4;
take n ; :: thesis: for m being Nat st n <= m holds
g < (r (#) seq) . m
let m be Nat; :: thesis: ( n <= m implies g < (r (#) seq) . m )
assume n <= m ; :: thesis: g < (r (#) seq) . m
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: verum

end;

assume A7: r = 0 ; :: thesis: ( rng (r (#) seq) = {0} & r (#) seq is constant )
thus rng (r (#) seq) = {0} :: thesis: r (#) seq is constant

proof

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

proof

assume x in rng (r (#) seq) ; :: thesis: x in {0}
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: verum

end;

assume x in {0} ; :: thesis: x in rng (r (#) seq)
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: verum

end;

hence r (#) seq is constant by FUNCT_2:111, Lm4; :: thesis: verum