|.s.| is convergent

proof

consider g being Element of COMPLEX such that
A1: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of 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 number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
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) - |.g.|) < p )
assume A2: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
p is Real by XREAL_0:def 1;
then consider n being Element of NAT such that
A3: for m being Element of NAT st n <= m holds
|.((s . m) - g).| < p by A1, A2;
take n ; :: thesis: for m being Element of NAT st n <= m holds
abs ((|.s.| . m) - |.g.|) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((|.s.| . m) - |.g.|) < p )
assume n <= m ; :: thesis: abs ((|.s.| . m) - |.g.|) < p
then |.((s . m) - g).| < p by A3;
then (abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).| < p + |.((s . m) - g).| by COMPLEX1:64, XREAL_1:8;
then ((abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).|) - |.((s . m) - g).| < (p + |.((s . m) - g).|) - |.((s . m) - g).| by XREAL_1:9;
hence abs ((|.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