let s be Complex_Sequence; :: thesis: ( s is convergent implies lim (s *') = (lim s) *' )
set g = lim s;
assume A1: s is convergent ; :: thesis: lim (s *') = (lim s) *'
then reconsider s1 = s as convergent Complex_Sequence ;

A2: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((s . m) - (lim s)).| < p by A1, Def6;
take n = n; :: thesis: for m being Nat st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((s *') . m) - ((lim s) *')).| < p )
assume A4: n <= m ; :: thesis: |.(((s *') . m) - ((lim s) *')).| < p
m in NAT by ORDINAL1:def 12;
then |.(((s *') . m) - ((lim s) *')).| = |.(((s . m) *') - ((lim s) *')).| by Def2
.= |.(((s . m) - (lim s)) *').| by COMPLEX1:34
.= |.((s . m) - (lim s)).| by COMPLEX1:53 ;
hence |.(((s *') . m) - ((lim s) *')).| < p by A3, A4; :: thesis: verum

end;

s1 *' is convergent ;
hence lim (s *') = (lim s) *' by A2, Def6; :: thesis: verum