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 ;
reconsider w = |.s1.| as Real_Sequence ;
A2: w is convergent ;
reconsider w = |.(lim s).| as Real ;

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) - w).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((|.s.| . m) - w).| < p )
assume A3: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((|.s.| . m) - w).| < p
consider n being Nat such that
A4: for m being Nat st n <= m holds
|.((s . m) - (lim s)).| < p by A1, A3, COMSEQ_2:def 6;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((|.s.| . m) - w).| < p
let m be Nat; :: thesis: ( n <= m implies |.((|.s.| . m) - w).| < p )
assume n <= m ; :: thesis: |.((|.s.| . m) - w).| < p
then |.((s . m) - (lim s)).| < p by A4;
then |.(|.(s . m).| - |.(lim s).|).| + |.((s . m) - (lim s)).| < p + |.((s . m) - (lim s)).| by COMPLEX1:64, XREAL_1:8;
then (|.(|.(s . m).| - |.(lim s).|).| + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| < (p + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| by XREAL_1:9;
hence |.((|.s.| . m) - w).| < p by VALUED_1:18; :: thesis: verum

end;

hence lim |.s.| = |.(lim s).| by A2, Def6; :: thesis: verum