|.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 Def4;
take R = |.g.|; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((|.s.| . b₃) - R) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((|.s.| . b₂) - R) ) )
assume A2: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((|.s.| . b₂) - R) )
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 b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((|.s.| . b₁) - R) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((|.s.| . m) - R) )
assume n <= m ; :: thesis: not p <= abs ((|.s.| . m) - R)
then |.((s . m) - g).| < p by A3;
then (abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).| < p + |.((s . m) - g).| by COMPLEX1:150, XREAL_1:10;
then ((abs (|.(s . m).| - |.g.|)) + |.((s . m) - g).|) - |.((s . m) - g).| < (p + |.((s . m) - g).|) - |.((s . m) - g).| by XREAL_1:11;
hence not p <= abs ((|.s.| . m) - R) by VALUED_1:18; :: thesis: verum

end;

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