|.s.| is convergent

proof

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

end;

hence for b₁ being Real_Sequence st b₁ = |.s.| holds
b₁ is convergent ; :: thesis: verum