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

now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p )
A3: p is Real by XREAL_0:def 1;
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p
then consider n being Element of NAT such that
A4: for m being Element of NAT st n <= m holds
|.((s . m) - (lim s)).| < p by A1, A3, Def5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - w) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((|.s.| . m) - w) < p )
assume n <= m ; :: thesis: abs ((|.s.| . m) - w) < p
then |.((s . m) - (lim s)).| < p by A4;
then (abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).| < p + |.((s . m) - (lim s)).| by COMPLEX1:150, XREAL_1:10;
then ((abs (|.(s . m).| - |.(lim s).|)) + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| < (p + |.((s . m) - (lim s)).|) - |.((s . m) - (lim s)).| by XREAL_1:11;
hence abs ((|.s.| . m) - w) < p by VALUED_1:18; :: thesis: verum

end;

hence lim |.s.| = |.(lim s).| by A2, SEQ_2:def 7; :: thesis: verum