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

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
|.(((s *') . m) - ((lim s) *')).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
|.((s . m) - (lim s)).| < p by A1, Def5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
|.(((s *') . m) - ((lim s) *')).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s *') . m) - ((lim s) *')).| < p )
assume A4: n <= m ; :: thesis: |.(((s *') . m) - ((lim s) *')).| < p
|.(((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, Def5; :: thesis: verum