let seq be Real_Sequence; :: thesis: ( seq is convergent implies abs seq is convergent )
assume seq is convergent ; :: thesis: abs seq is convergent
then consider g1 being Real such that
A1: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < p ;
reconsider g1 = g1 as Real ;
take g = |.g1.|; :: according to SEQ_2:def 6 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.(((abs seq) . b₃) - g).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((abs seq) . b₂) - g).| ) )
assume 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((abs seq) . b₂) - g).| )
then consider n1 being Nat such that
A2: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < p by A1;
take n = n1; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= |.(((abs seq) . b₁) - g).| )
let m be Nat; :: thesis: ( not n <= m or not p <= |.(((abs seq) . m) - g).| )
|.(g1 - (seq . m)).| = |.(- ((seq . m) - g1)).|
.= |.((seq . m) - g1).| by COMPLEX1:52 ;
then g - |.(seq . m).| <= |.((seq . m) - g1).| by COMPLEX1:59;
then ( |.(seq . m).| - g <= |.((seq . m) - g1).| & - |.((seq . m) - g1).| <= - (g - |.(seq . m).|) ) by COMPLEX1:59, XREAL_1:24;
then |.(|.(seq . m).| - g).| <= |.((seq . m) - g1).| by ABSVALUE:5;
then A3: |.(((abs seq) . m) - g).| <= |.((seq . m) - g1).| by SEQ_1:12;
assume n <= m ; :: thesis: not p <= |.(((abs seq) . m) - g).|
then |.((seq . m) - g1).| < p by A2;
hence not p <= |.(((abs seq) . m) - g).| by A3, XXREAL_0:2; :: thesis: verum