X: c in COMPLEX by XCMPLX_0:def 2;

now

let c be Element of COMPLEX ; :: thesis: b₁ (#) s is convergent

per cases ( c = 0c or c <> 0c ) ;

suppose A3: c = 0c ; :: thesis: b₁ (#) s is convergent

now

let n be Element of NAT ; :: thesis: (c (#) s) . n = 0c
thus (c (#) s) . n = 0c * (s . n) by A3, VALUED_1:6
.= 0c ; :: thesis: verum

end;

hence c (#) s is convergent by Th9; :: thesis: verum

end;

suppose A4: c <> 0c ; :: thesis: b₁ (#) s is convergent

thus c (#) s is convergent :: thesis: verum

proof

A5: |.c.| > 0 by A4, COMPLEX1:133;
then A6: |.c.| " > 0 ;
consider g being Element of COMPLEX such that
A7: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by Def4;
take g' = c * g; :: according to COMSEQ_2:def 4 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g').| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g').| < p )
assume A8: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g').| < p
p / |.c.| = p * (|.c.| " ) by XCMPLX_0:def 9;
then p / |.c.| > 0 by A6, A8, XREAL_1:131;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p / |.c.| by A7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.(((c (#) s) . m) - g').| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((c (#) s) . m) - g').| < p )
assume n <= m ; :: thesis: |.(((c (#) s) . m) - g').| < p
then A10: |.((s . m) - g).| < p / |.c.| by A9;
A11: |.(((c (#) s) . m) - g').| = |.((c * (s . m)) - (c * g)).| by VALUED_1:6
.= |.(c * ((s . m) - g)).|
.= |.((s . m) - g).| * |.c.| by COMPLEX1:151 ;
|.((s . m) - g).| * |.c.| < (p / |.c.|) * |.c.| by A5, A10, XREAL_1:70;
then |.((s . m) - g).| * |.c.| < (p * (|.c.| " )) * |.c.| by XCMPLX_0:def 9;
then |.((s . m) - g).| * |.c.| < p * ((|.c.| " ) * |.c.|) ;
then |.((s . m) - g).| * |.c.| < p * 1 by A5, XCMPLX_0:def 7;
hence |.(((c (#) s) . m) - g').| < p by A11; :: thesis: verum

end;

end;

end;

end;

hence for b₁ being Complex_Sequence st b₁ = c (#) s holds
b₁ is convergent by X; :: thesis: verum