let r be real number ; :: thesis: for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent
let seq be Real_Sequence; :: thesis: ( seq is convergent implies r (#) seq is convergent )
assume seq is convergent ; :: thesis: r (#) seq is convergent
then consider g1 being real number such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by Def6;
take g = r * g1; :: according to SEQ_2:def 6 :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((r (#) seq) . m) - g) < p

A2: now

assume A3: r = 0 ; :: thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let p be real number ; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p )
assume A4: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
take k = 0 ; :: thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((r (#) seq) . m) - g) < p )
assume k <= m ; :: thesis: abs (((r (#) seq) . m) - g) < p
abs (((r (#) seq) . m) - g) = abs ((0 * (seq . m)) - 0 ) by A3, SEQ_1:13
.= 0 by ABSVALUE:7 ;
hence abs (((r (#) seq) . m) - g) < p by A4; :: thesis: verum

end;

now

assume A5: r <> 0 ; :: thesis: for p being real number st 0 < p holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
then A6: 0 < abs r by COMPLEX1:133;
let p be real number ; :: thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p )
assume A7: 0 < p ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
A8: 0 <> abs r by A5, COMPLEX1:133;
0 / (abs r) = 0 ;
then 0 < p / (abs r) by A6, A7, XREAL_1:76;
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / (abs r) by A1;
take k = n1; :: thesis: for m being Element of NAT st k <= m holds
abs (((r (#) seq) . m) - g) < p
let m be Element of NAT ; :: thesis: ( k <= m implies abs (((r (#) seq) . m) - g) < p )
assume k <= m ; :: thesis: abs (((r (#) seq) . m) - g) < p
then A10: abs ((seq . m) - g1) < p / (abs r) by A9;
A11: abs (((r (#) seq) . m) - g) = abs ((r * (seq . m)) - (r * g1)) by SEQ_1:13
.= abs (r * ((seq . m) - g1))
.= (abs r) * (abs ((seq . m) - g1)) by COMPLEX1:151 ;
(abs r) * (p / (abs r)) = (abs r) * (((abs r) " ) * p) by XCMPLX_0:def 9
.= ((abs r) * ((abs r) " )) * p
.= 1 * p by A8, XCMPLX_0:def 7
.= p ;
hence abs (((r (#) seq) . m) - g) < p by A6, A10, A11, XREAL_1:70; :: thesis: verum

end;

hence for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((r (#) seq) . m) - g) < p by A2; :: thesis: verum