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

proof

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

proof

now

let e be real number ; :: thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e )
assume A6: e > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e :: thesis: verum

proof

e is Real by XREAL_0:def 1;
then consider k being Element of NAT such that
A7: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A6, Th10;
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e

proof

let m be Element of NAT ; :: thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A8: k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
||.((vseq . m) - (vseq . k)).|| = Sum (abs (seq_id ((vseq . m) - (vseq . k)))) by Th8;
then A9: Sum (abs (seq_id ((vseq . m) - (vseq . k)))) < e by A7, A8;
seq_id ((vseq . m) - (vseq . k)) is absolutely_summable by Def1;
then A10: abs (seq_id ((vseq . m) - (vseq . k))) is summable by SERIES_1:def 5;
for i being Element of NAT holds 0 <= (abs (seq_id ((vseq . m) - (vseq . k)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (abs (seq_id ((vseq . m) - (vseq . k)))) . i
0 <= abs ((seq_id ((vseq . m) - (vseq . k))) . i) by COMPLEX1:132;
hence 0 <= (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:16; :: thesis: verum

end;

then A11: (abs (seq_id ((vseq . m) - (vseq . k)))) . i <= Sum (abs (seq_id ((vseq . m) - (vseq . k)))) by A10, RSSPACE2:4;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th8
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:3
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by SEQ_1:15 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:11
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:14
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A4
.= (rseqi . m) - (rseqi . k) by A4 ;
then abs ((rseqi . m) - (rseqi . k)) = (abs (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:16;
hence abs ((rseqi . m) - (rseqi . k)) < e by A9, A11, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ; :: thesis: verum

end;

end;

hence rseqi is convergent by SEQ_4:58; :: thesis: verum

end;

take y = lim rseqi; :: thesis: ( y in REAL & S₁[x,y] )
thus ( y in REAL & S₁[x,y] ) by A4, A5; :: thesis: verum

end;

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

A13: now

let i be Element of NAT ; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A12;
hence ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum

end;

A14: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of 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 Element of NAT st
for n being Element of 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 A15: e1 > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of 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 )
set e = e1 / 2;
A16: e1 / 2 > 0 by A15, XREAL_1:217;
A17: e1 / 2 < e1 by A15, XREAL_1:218;
consider k being Element of NAT such that
A18: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, A16, Th10;
A19: for m, n being Element of 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 Element of NAT holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) )

proof

let m, n be Element of 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 Element of NAT holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) ) )
assume A20: ( 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 Element of NAT holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) )
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A18, A20;
then A21: the norm of l1_Space . ((vseq . n) - (vseq . m)) < e1 / 2 by NORMSP_1:def 1;
A22: seq_id ((vseq . n) - (vseq . m)) is absolutely_summable by Def1;
for i being Element of NAT holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i
0 <= abs ((seq_id ((vseq . n) - (vseq . m))) . i) by COMPLEX1:132;
hence 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i by SEQ_1:16; :: thesis: verum

end;

hence ( abs (seq_id ((vseq . n) - (vseq . m))) is summable & Sum (abs (seq_id ((vseq . n) - (vseq . m)))) < e1 / 2 & ( for i being Element of NAT holds 0 <= (abs (seq_id ((vseq . n) - (vseq . m)))) . i ) ) by A21, A22, Def2, SERIES_1:def 5; :: thesis: verum

end;

A23: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 Element of NAT ; :: thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 )
A24: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))

proof

let m, k be Element of 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 Th8;
hence seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:3; :: thesis: verum

end;

defpred S₂[ Element of NAT ] means for rseq being Real_Sequence st ( for m being Element of 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 );
A25: S₂[ 0 ]

proof

now

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of 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 A26: for m being Element of 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
A27: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 ) & rseq0 is convergent & tseq . 0 = lim rseq0 ) by A13;
A28: for m being Element of NAT holds rseq . m = abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0 ))

proof

let m be Element of NAT ; :: thesis: rseq . m = abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0 ))
rseq . m = (Partial_Sums (abs (seq_id ((vseq . m) - (vseq . n))))) . 0 by A26
.= (abs (seq_id ((vseq . m) - (vseq . n)))) . 0 by SERIES_1:def 1
.= (abs ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . 0 by A24
.= (abs ((seq_id (vseq . m)) + (- (seq_id (vseq . n))))) . 0 by SEQ_1:15
.= abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:16
.= abs (((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:11
.= abs (((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) by SEQ_1:14
.= abs (((seq_id (vseq . m)) . 0 ) - ((seq_id (vseq . n)) . 0 )) ;
hence rseq . m = abs ((rseq0 . m) - ((seq_id (vseq . n)) . 0 )) by A27; :: thesis: verum

end;

then lim rseq = abs ((lim rseq0) - ((seq_id (vseq . n)) . 0 )) by A27, Th1
.= abs ((tseq . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) by A27
.= abs ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:14
.= abs ((tseq + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:11
.= abs ((tseq - (seq_id (vseq . n))) . 0 ) by SEQ_1:15
.= abs (((seq_id tseq) - (seq_id (vseq . n))) . 0 ) by RSSPACE:3
.= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . 0 by SEQ_1:16
.= (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 A27, A28, Th1; :: thesis: verum

end;

end;

hence S₂[ 0 ] ; :: thesis: verum

end;

A29: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

now

let i be Element of NAT ; :: thesis: ( ( for rseq being Real_Sequence st ( for m being Element of 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 Element of 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 A30: for rseq being Real_Sequence st ( for m being Element of 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 Element of 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 Element of 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

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of 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 A31: for m being Element of 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) )
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums (abs (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseqb being Real_Sequence such that
A32: for m being Element of NAT holds rseqb . m = H₁(m) from SEQ_1:sch 1();
A33: ( rseqb is convergent & lim rseqb = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i ) by A30, A32;
consider rseq0 being Real_Sequence such that
A34: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) ) & rseq0 is convergent & tseq . (i + 1) = lim rseq0 ) by A13;

A35: now

let m be Element of NAT ; :: thesis: rseq . m = (abs ((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 A31
.= ((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 A24
.= ((abs ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + (rseqb . m) by A32
.= (abs (((seq_id (vseq . m)) - (seq_id (vseq . n))) . (i + 1))) + (rseqb . m) by SEQ_1:16
.= (abs (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1))) + (rseqb . m) by SEQ_1:15
.= (abs (((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (rseqb . m) by SEQ_1:11
.= (abs (((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (rseqb . m) by SEQ_1:14
.= (abs (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m)
.= (abs ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A34 ; :: thesis: verum

end;

then lim rseq = (abs ((lim rseq0) - ((seq_id (vseq . n)) . (i + 1)))) + (lim rseqb) by A33, A34, Lm4
.= (abs ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (lim rseqb) by A34
.= (abs ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:14
.= (abs ((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:15
.= ((abs (tseq - (seq_id (vseq . n)))) . (i + 1)) + (lim rseqb) by SEQ_1:16
.= ((abs (tseq - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i) by A30, A32
.= ((abs ((seq_id tseq) - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i) by RSSPACE:3
.= (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 A33, A34, A35, Lm4; :: thesis: verum

end;

end;

hence for i being Element of NAT st S₂[i] holds
S₂[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A25, A29);
hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of 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 Element of 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 Element of 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 Element of NAT st 0 <= i holds
(Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2

proof

let i be Element of 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₁( Element of NAT ) -> Element of REAL = (Partial_Sums (abs (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseq being Real_Sequence such that
A38: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A39: rseq is convergent by A23, A38;
A40: lim rseq = (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i by A23, A38;
for m being Element of NAT st m >= k holds
rseq . m <= e1 / 2

proof

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

end;

hence (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i <= e1 / 2 by A39, A40, RSSPACE2:6; :: thesis: verum

end;

A43: for i being Element of NAT holds 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i
(abs ((seq_id tseq) - (seq_id (vseq . n)))) . i = abs (((seq_id tseq) - (seq_id (vseq . n))) . i) by SEQ_1:16;
hence 0 <= (abs ((seq_id tseq) - (seq_id (vseq . n)))) . i by COMPLEX1:132; :: thesis: verum

end;

A44: Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above

proof

now

take e1 = e1; :: thesis: for i being Element of NAT holds (Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1
let i be Element of 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 A17, XXREAL_0:2; :: thesis: verum

end;

hence Partial_Sums (abs ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

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

end;

hence ex k being Element of NAT st
for n being Element of 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

A46: for i being Element of NAT holds 0 <= (abs (seq_id tseq)) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (abs (seq_id tseq)) . i
(abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:16;
hence 0 <= (abs (seq_id tseq)) . i by COMPLEX1:132; :: thesis: verum

end;

consider m being Element of NAT such that
A47: for n being Element of 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 A14;
A48: abs ((seq_id tseq) - (seq_id (vseq . m))) is summable by A47;
seq_id (vseq . m) is absolutely_summable by Def1;
then A49: abs (seq_id (vseq . m)) is summable by SERIES_1:def 5;
set a = abs ((seq_id tseq) - (seq_id (vseq . m)));
set b = abs (seq_id (vseq . m));
set d = abs (seq_id tseq);
A50: (abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m))) is summable by A48, A49, SERIES_1:10;
for i being Element of 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 Element of NAT ; :: thesis: (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i
A51: (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i = abs (((seq_id tseq) - (seq_id (vseq . m))) . i) by SEQ_1:16
.= abs (((seq_id tseq) + (- (seq_id (vseq . m)))) . i) by SEQ_1:15
.= abs (((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)) by SEQ_1:11
.= abs (((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))) by SEQ_1:14
.= abs (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) ;
A52: (abs (seq_id (vseq . m))) . i = abs ((seq_id (vseq . m)) . i) by SEQ_1:16;
(abs (seq_id tseq)) . i = abs ((seq_id tseq) . i) by SEQ_1:16;
then ((abs (seq_id tseq)) . i) - ((abs (seq_id (vseq . m))) . i) <= (abs ((seq_id tseq) - (seq_id (vseq . m)))) . i by A51, A52, COMPLEX1:145;
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:8;
hence (abs (seq_id tseq)) . i <= ((abs ((seq_id tseq) - (seq_id (vseq . m)))) + (abs (seq_id (vseq . m)))) . i by SEQ_1:11; :: thesis: verum

end;

hence abs (seq_id tseq) is summable by A46, A50, SERIES_1:24; :: thesis: verum

end;

then A53: seq_id tseq is absolutely_summable by SERIES_1:def 5;
A54: tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider tv = tseq as Point of l1_Space by A53, Def1;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e

proof

let e be Real; :: thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A55: e > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT such that
A56: for n being Element of 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 A14, A55;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A57: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
reconsider u = tseq as VECTOR of l1_Space by A53, A54, Def1;
A58: Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) < e by A56, A57;
reconsider v = vseq . n as VECTOR of l1_Space ;
seq_id (u - v) = u - v by Th8;
then Sum (abs (seq_id (u - v))) = Sum (abs ((seq_id tseq) - (seq_id (vseq . n)))) by Th8;
then A59: the norm of l1_Space . (u - v) < e by A58, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:47
.= ||.(tv - (vseq . n)).|| by NORMSP_1:6 ;
hence ||.((vseq . n) - tv).|| < e by A59, NORMSP_1:def 1; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum

end;

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