let s be Complex_Sequence; :: thesis: for r being complex number st s is convergent holds
lim (r (#) s) = r * (lim s)
let r be complex number ; :: thesis: ( s is convergent implies lim (r (#) s) = r * (lim s) )
assume A1: s is convergent ; :: thesis: lim (r (#) s) = r * (lim s)
then A2: r (#) s is convergent ;
reconsider r = r as Element of COMPLEX by XCMPLX_0:def 2;

A3: now

assume A4: r = 0c ; :: thesis: lim (r (#) s) = r * (lim s)

now

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

end;

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

end;

now

assume A5: r <> 0c ; :: thesis: ( ( for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p ) & lim (r (#) s) = r * (lim s) )
thus for p being Real st p > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p :: thesis: lim (r (#) s) = r * (lim s)

proof

A6: |.r.| > 0 by A5, COMPLEX1:133;
then A7: |.r.| " > 0 ;
let p be Real; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p )
assume A8: p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
p / |.r.| = p * (|.r.| " ) by XCMPLX_0:def 9;
then p / |.r.| > 0 by A7, 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) - (lim s)).| < p / |.r.| by A1, Def5;
take n ; :: thesis: for m being Element of NAT st n <= m holds
|.(((r (#) s) . m) - (r * (lim s))).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((r (#) s) . m) - (r * (lim s))).| < p )
assume n <= m ; :: thesis: |.(((r (#) s) . m) - (r * (lim s))).| < p
then A10: |.((s . m) - (lim s)).| < p / |.r.| by A9;
A11: |.(((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:151 ;
|.((s . m) - (lim s)).| * |.r.| < (p / |.r.|) * |.r.| by A6, A10, XREAL_1:70;
then |.((s . m) - (lim s)).| * |.r.| < (p * (|.r.| " )) * |.r.| by XCMPLX_0:def 9;
then |.((s . m) - (lim s)).| * |.r.| < p * ((|.r.| " ) * |.r.|) ;
then |.((s . m) - (lim s)).| * |.r.| < p * 1 by A6, XCMPLX_0:def 7;
hence |.(((r (#) s) . m) - (r * (lim s))).| < p by A11; :: thesis: verum

end;

hence lim (r (#) s) = r * (lim s) by A2, Def5; :: thesis: verum

end;

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