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

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:120
.= |.((s . m) - (lim s)).| by COMPLEX1:139 ;
hence |.(((s *' ) . m) - ((lim s) *' )).| < p by A3, A4; :: thesis: verum

end;

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