let vseq be sequence of l1_Space; :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
defpred S₁[ object , object ] means ex i being Nat st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider i = x as Nat ;
deffunc H₁( Nat) -> set = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A3: for n being Nat holds rseqi . n = H₁(n) from SEQ_1:sch 1();
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr ; :: thesis: ( lr in REAL & S₁[x,lr] )

now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e )
assume A4: e > 0 ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
thus ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e :: thesis: verum

proof

consider k being Nat such that
A5: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, Th8;
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e

proof

let m be Nat; :: thesis: ( k <= m implies |.((rseqi . m) - (rseqi . k)).| < e )
assume A6: k <= m ; :: thesis: |.((rseqi . m) - (rseqi . k)).| < e
A7: for i being Nat holds 0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i

proof

let i be Nat; :: thesis: 0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i
0 <= |.((seq_id ((vseq . m) - (vseq . k))) . i).| by COMPLEX1:46;
hence 0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i by SEQ_1:12; :: thesis: verum

end;

seq_id ((vseq . m) - (vseq . k)) is absolutely_summable by Def1;
then abs (seq_id ((vseq . m) - (vseq . k))) is summable by SERIES_1:def 4;
then A8: (abs (seq_id ((vseq . m) - (vseq . k)))) . i <= Sum |.(seq_id ((vseq . m) - (vseq . k))).| by A7, RSSPACE2:3;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th6
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by SEQ_1:11 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then A9: |.((rseqi . m) - (rseqi . k)).| = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:12;
||.((vseq . m) - (vseq . k)).|| = Sum |.(seq_id ((vseq . m) - (vseq . k))).| by Th6;
then Sum |.(seq_id ((vseq . m) - (vseq . k))).| < e by A5, A6;
hence |.((rseqi . m) - (rseqi . k)).| < e by A8, A9, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e ; :: thesis: verum

end;

end;

then rseqi is convergent by SEQ_4:41;
hence ( lr in REAL & S₁[x,lr] ) by A3; :: thesis: verum

end;

consider f being sequence of REAL such that
A10: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider tseq = f as Real_Sequence ;

A11: now :: thesis: for i being Nat ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )

let i be Nat; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
i in NAT by ORDINAL1:def 12;
then ex i0 being Nat st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A10;
hence ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum

end;

A12: for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e )

proof

let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 ) )
assume A13: e1 > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 )
reconsider e1 = e1 as Real ;
set e = e1 / 2;
A14: e1 / 2 < e1 by A13, XREAL_1:216;
e1 / 2 > 0 by A13, XREAL_1:215;
then consider k being Nat such that
A15: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, Th8;
A16: for m, n being Nat st n >= k & m >= k holds
( abs (seq_id ((vseq . n) - (vseq . m))) is summable & Sum (abs (seq_id ((vseq . n) - (vseq . m)))) < e1 / 2 & ( for i being Nat holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) )

proof

let m, n be Nat; :: thesis: ( n >= k & m >= k implies ( abs (seq_id ((vseq . n) - (vseq . m))) is summable & Sum (abs (seq_id ((vseq . n) - (vseq . m)))) < e1 / 2 & ( for i being Nat holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) ) )
assume ( n >= k & m >= k ) ; :: thesis: ( abs (seq_id ((vseq . n) - (vseq . m))) is summable & Sum (abs (seq_id ((vseq . n) - (vseq . m)))) < e1 / 2 & ( for i being Nat holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) )
then ||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A15;
then A17: the normF of l1_Space . ((vseq . n) - (vseq . m)) < e1 / 2 ;
A18: for i being Nat holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i

proof

let i be Nat; :: thesis: 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i
0 <= |.((seq_id ((vseq . n) - (vseq . m))) . i).| by COMPLEX1:46;
hence 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i by SEQ_1:12; :: thesis: verum

end;

seq_id ((vseq . n) - (vseq . m)) is absolutely_summable by Def1;
hence ( abs (seq_id ((vseq . n) - (vseq . m))) is summable & Sum (abs (seq_id ((vseq . n) - (vseq . m)))) < e1 / 2 & ( for i being Nat holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) ) by A17, A18, Def2, SERIES_1:def 4; :: thesis: verum

end;

A19: for n, i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i )

proof

let n be Nat; :: thesis: for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i )
defpred S₂[ Nat] means for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . $1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . $1 );
A20: for m, k being Nat holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))

proof

let m, k be Nat; :: thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th6;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) ; :: thesis: verum

end;

now :: thesis: for i being Nat st ( for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ) holds
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) )

let i be Nat; :: thesis: ( ( for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ) implies for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) )
assume A21: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ; :: thesis: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) )
thus for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) :: thesis: verum

proof

deffunc H₁( Nat) -> set = (Partial_Sums (abs (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseqb being Real_Sequence such that
A22: for m being Nat holds rseqb . m = H₁(m) from SEQ_1:sch 1();
consider rseq0 being Real_Sequence such that
A23: for m being Nat holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A24: rseq0 is convergent and
A25: tseq . (i + 1) = lim rseq0 by A11;
let rseq be Real_Sequence; :: thesis: ( ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) )
assume A26: for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) )

A27: now :: thesis: for m being Nat holds rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)

let m be Nat; :: thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)
thus rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) by A26
.= ((abs (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + ((Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i) by SERIES_1:def 1
.= ((abs ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i) by A20
.= ((abs ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + (rseqb . m) by A22
.= |.(((seq_id (vseq . m)) - (seq_id (vseq . n))) . (i + 1)).| + (rseqb . m) by SEQ_1:12
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).| + (rseqb . m) by SEQ_1:11
.= |.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| + (rseqb . m) by SEQ_1:7
.= |.(((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).| + (rseqb . m) by SEQ_1:10
.= |.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m) by A23 ; :: thesis: verum

end;

A28: rseqb is convergent by A21, A22;
then lim rseq = |.((lim rseq0) - ((seq_id (vseq . n)) . (i + 1))).| + (lim rseqb) by A24, A27, Lm3
.= |.((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).| + (lim rseqb) by A25
.= |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| + (lim rseqb) by SEQ_1:10
.= |.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).| + (lim rseqb) by SEQ_1:7
.= |.((tseq - (seq_id (vseq . n))) . (i + 1)).| + (lim rseqb) by SEQ_1:11
.= ((abs (tseq - (seq_id (vseq . n)))) . (i + 1)) + (lim rseqb) by SEQ_1:12
.= ((abs (tseq - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i) by A21, A22
.= (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) by SERIES_1:def 1 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) by A28, A24, A27, Lm3; :: thesis: verum

end;

end;

then A29: for i being Nat st S₂[i] holds
S₂[i + 1] ;

now :: thesis: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . 0 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 )

let rseq be Real_Sequence; :: thesis: ( ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) )
assume A30: for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . 0 ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 )
thus ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) :: thesis: verum

proof

consider rseq0 being Real_Sequence such that
A31: for m being Nat holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A32: rseq0 is convergent and
A33: tseq . 0 = lim rseq0 by A11;
A34: for m being Nat holds rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|

proof

let m be Nat; :: thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|
rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . 0 by A30
.= (abs (seq_id ((vseq . m) - (vseq . n)))) . 0 by SERIES_1:def 1
.= (abs ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . 0 by A20
.= (abs ((seq_id (vseq . m)) + (- (seq_id (vseq . n))))) . 0 by SEQ_1:11
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| by SEQ_1:12
.= |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| by SEQ_1:7
.= |.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))).| by SEQ_1:10
.= |.(((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)).| ;
hence rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| by A31; :: thesis: verum

end;

then lim rseq = |.((lim rseq0) - ((seq_id (vseq . n)) . 0)).| by A32, Th1
.= |.((tseq . 0) + (- ((seq_id (vseq . n)) . 0))).| by A33
.= |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| by SEQ_1:10
.= |.((tseq + (- (seq_id (vseq . n)))) . 0).| by SEQ_1:7
.= |.((tseq - (seq_id (vseq . n))) . 0).| by SEQ_1:11
.= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . 0 by SEQ_1:12
.= (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 by SERIES_1:def 1 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) by A32, A34, Th1; :: thesis: verum

end;

end;

then A35: S₂[ 0 ] ;
for i being Nat holds S₂[i] from NAT_1:sch 2(A35, A29);
hence for i being Nat
for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ; :: thesis: verum

end;

for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 )

proof

let n be Nat; :: thesis: ( n >= k implies ( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 ) )
assume A36: n >= k ; :: thesis: ( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 )
A37: for i being Nat st 0 <= i holds
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2

proof

let i be Nat; :: thesis: ( 0 <= i implies (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2 )
assume 0 <= i ; :: thesis: (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2
deffunc H₁( Nat) -> set = (Partial_Sums (abs (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseq being Real_Sequence such that
A38: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();
A39: for m being Nat st m >= k holds
rseq . m <= e1 / 2

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= e1 / 2 )
A40: rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i by A38;
assume A41: m >= k ; :: thesis: rseq . m <= e1 / 2
then ( abs (seq_id ((vseq . m) - (vseq . n))) is summable & ( for i being Nat holds 0 <= (abs (seq_id ((vseq . m) - (vseq . n)))) . i ) ) by A16, A36;
then A42: (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . i <= Sum (abs (seq_id ((vseq . m) - (vseq . n)))) by RSSPACE2:3;
Sum (abs (seq_id ((vseq . m) - (vseq . n)))) < e1 / 2 by A16, A36, A41;
hence rseq . m <= e1 / 2 by A42, A40, XXREAL_0:2; :: thesis: verum

end;

( rseq is convergent & lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) by A19, A38;
hence (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2 by A39, RSSPACE2:5; :: thesis: verum

end;

now :: thesis: ex e1 being Real st
for i being Nat holds (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1

take e1 = e1; :: thesis: for i being Nat holds (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1
let i be Nat; :: thesis: (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2 by A37, NAT_1:2;
hence (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 by A14, XXREAL_0:2; :: thesis: verum

end;

then A43: Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above by SEQ_2:def 3;
A44: for i being Nat holds 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i

proof

let i be Nat; :: thesis: 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i
(abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = |.(((seq_id tseq) - (seq_id (vseq . n))) . i).| by SEQ_1:12;
hence 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by COMPLEX1:46; :: thesis: verum

end;

then abs ((seq_id tseq) - (seq_id (vseq . n))) is summable by A43, SERIES_1:17;
then Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n)))) is convergent by SERIES_1:def 2;
then ( Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) = lim (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) & lim (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) <= e1 / 2 ) by A37, RSSPACE2:5, SERIES_1:def 3;
hence ( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 ) by A14, A44, A43, SERIES_1:17, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Nat st
for n being Nat st n >= k holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e1 ) ; :: thesis: verum

end;

abs (seq_id tseq) is summable

proof

set d = abs (seq_id tseq);
A45: for i being Nat holds 0 <= (abs (seq_id tseq)) . i

proof

let i be Nat; :: thesis: 0 <= (abs (seq_id tseq)) . i
(abs (seq_id tseq)) . i = |.((seq_id tseq) . i).| by SEQ_1:12;
hence 0 <= (abs (seq_id tseq)) . i by COMPLEX1:46; :: thesis: verum

end;

consider m being Nat such that
A46: for n being Nat st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < 1 ) by A12;
set b = abs (seq_id (vseq . m));
set a = abs ((seq_id tseq) - (seq_id (vseq . m)));
seq_id (vseq . m) is absolutely_summable by Def1;
then A47: abs (seq_id (vseq . m)) is summable by SERIES_1:def 4;
A48: for i being Nat holds (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i

proof

let i be Nat; :: thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
A49: ( (abs (seq_id (vseq . m))) . i = |.((seq_id (vseq . m)) . i).| & (abs (seq_id tseq)) . i = |.((seq_id tseq) . i).| ) by SEQ_1:12;
(abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = |.(((seq_id tseq) - (seq_id (vseq . m))) . i).| by SEQ_1:12
.= |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by SEQ_1:11
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by SEQ_1:7
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by SEQ_1:10
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A49, COMPLEX1:59;
then (((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i)) + ((abs (seq_id (vseq . m))) . i) <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) . i) + ((abs (seq_id (vseq . m))) . i) by XREAL_1:6;
hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:7; :: thesis: verum

end;

abs ((seq_id tseq) - (seq_id (vseq . m))) is summable by A46;
then (abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))) is summable by A47, SERIES_1:7;
hence abs (seq_id tseq) is summable by A45, A48, SERIES_1:20; :: thesis: verum

end;

then A50: seq_id tseq is absolutely_summable by SERIES_1:def 4;
A51: tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider tv = tseq as Point of l1_Space by A50, Def1;
for e being Real st e > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

proof

let e be Real; :: thesis: ( e > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e )
assume e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
then consider m being Nat such that
A52: for n being Nat st n >= m holds
( abs ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e ) by A12;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
reconsider u = tseq as VECTOR of l1_Space by A50, A51, Def1;
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
then A53: Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e by A52;
reconsider v = vseq . n as VECTOR of l1_Space ;
seq_id (u - v) = u - v by Th6;
then Sum (abs (seq_id (u - v))) = Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) by Th6;
then A54: the normF of l1_Space . (u - v) < e by A53, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by NORMSP_1:2 ;
hence ||.((vseq . n) - tv).|| < e by A54; :: thesis: verum

end;

hence vseq is convergent by NORMSP_1:def 6; :: thesis: verum