let n be Nat; :: thesis: (c (#) s) . n = 0c
thus (c (#) s) . n = 0c * (s . n) by A2, VALUED_1:6
.= 0c ; :: thesis: verum

consider g being Complex such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((s . m) - g).| < p by Def5;
take g9 = c * g; :: according to COMSEQ_2:def 5 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((c (#) s) . m) - g9).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((c (#) s) . m) - g9).| < p )
assume A5: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((c (#) s) . m) - g9).| < p
A6: |.c.| > 0 by A3, COMPLEX1:47;
consider n being Nat such that
A7: for m being Nat st n <= m holds
|.((s . m) - g).| < p / |.c.| by A6, A4, A5;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((c (#) s) . m) - g9).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((c (#) s) . m) - g9).| < p )
assume n <= m ; :: thesis: |.(((c (#) s) . m) - g9).| < p
then |.((s . m) - g).| < p / |.c.| by A7;
then |.((s . m) - g).| * |.c.| < (p / |.c.|) * |.c.| by A6, XREAL_1:68;
then |.((s . m) - g).| * |.c.| < (p * (|.c.| ")) * |.c.| by XCMPLX_0:def 9;
then |.((s . m) - g).| * |.c.| < p * ((|.c.| ") * |.c.|) ;
then A8: |.((s . m) - g).| * |.c.| < p * 1 by A6, XCMPLX_0:def 7;
|.(((c (#) s) . m) - g9).| = |.((c * (s . m)) - (c * g)).| by VALUED_1:6
.= |.(c * ((s . m) - g)).|
.= |.((s . m) - g).| * |.c.| by COMPLEX1:65 ;
hence |.(((c (#) s) . m) - g9).| < p by A8; :: thesis: verum