let s be convergent Complex_Sequence; :: thesis: for r being Complex holds lim (r (#) s) = r * (lim s)
let r be Complex; :: thesis: lim (r (#) s) = r * (lim s)
reconsider r = r as Element of COMPLEX by XCMPLX_0:def 2;

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

suppose A1: r <> 0c ; :: thesis: lim (r (#) s) = r * (lim s)

for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p

proof

let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p )
assume A2: p > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
A3: |.r.| > 0 by A1, COMPLEX1:47;
p / |.r.| > 0 by A3, A2;
then consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((s . m) - (lim s)).| < p / |.r.| by Def6;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((r (#) s) . m) - (r * (lim s))).| < p )
assume n <= m ; :: thesis: |.(((r (#) s) . m) - (r * (lim s))).| < p
then |.((s . m) - (lim s)).| < p / |.r.| by A4;
then |.((s . m) - (lim s)).| * |.r.| < (p / |.r.|) * |.r.| by A3, XREAL_1:68;
then |.((s . m) - (lim s)).| * |.r.| < (p * (|.r.| ")) * |.r.| by XCMPLX_0:def 9;
then |.((s . m) - (lim s)).| * |.r.| < p * ((|.r.| ") * |.r.|) ;
then A5: |.((s . m) - (lim s)).| * |.r.| < p * 1 by A3, XCMPLX_0:def 7;
|.(((r (#) s) . m) - (r * (lim s))).| = |.((r * (s . m)) - (r * (lim s))).| by VALUED_1:6
.= |.(r * ((s . m) - (lim s))).|
.= |.((s . m) - (lim s)).| * |.r.| by COMPLEX1:65 ;
hence |.(((r (#) s) . m) - (r * (lim s))).| < p by A5; :: thesis: verum

end;

hence lim (r (#) s) = r * (lim s) by Def6; :: thesis: verum

end;

suppose A6: r = 0c ; :: thesis: lim (r (#) s) = r * (lim s)

now :: thesis: for n being Nat holds (r (#) s) . n = 0c

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

end;

hence lim (r (#) s) = r * (lim s) by A6, Th10; :: thesis: verum

end;

end;