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

proof

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

proof

now

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

proof

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, CLVECT_2:58;

now

let m be Element of NAT ; :: thesis: ( k <= m implies |.((seqi . m) - (seqi . k)).| < e )
assume A8: k <= m ; :: thesis: |.((seqi . m) - (seqi . k)).| < e
set vm = vseq . m;
set vk = vseq . k;
set seqmk = seq_id ((vseq . m) - (vseq . k));
||.((vseq . m) - (vseq . k)).|| < e by A7, A8;
then A9: sqrt |.(((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))).| < e by CSSPACE:def 15;
reconsider e1 = e as Real ;
|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.(seq_id ((vseq . m) - (vseq . k))).| is summable by CSSPACE:def 11, CSSPACE:def 20;
then A10: |.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).| is summable by Lm19;
A11: for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i
(|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i = (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.((seq_id ((vseq . m) - (vseq . k))) *' ).| . i) by SEQ_1:12
.= (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i) by Lm19 ;
hence 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i by XREAL_1:65; :: thesis: verum

end;

then A12: 0 <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) by A10, SERIES_1:21;
then A13: 0 <= sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|)) by SQUARE_1:def 4;
(seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' ) is absolutely_summable by Lm20;
then A14: (seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' ) is summable ;
for j being Element of NAT holds
( (Re ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' ))) . j >= 0 & (Im ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' ))) . j = 0 ) by Lm9;
then |.(Sum ((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' ))).| = Sum |.((seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *' )).| by A14, Lm8
.= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) by COMSEQ_1:49 ;
then sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|)) < e by A9, Lm18;
then (sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|))) ^2 < e1 ^2 by A13, SQUARE_1:78;
then A15: Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) < e * e by A12, SQUARE_1:def 4;
A16: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i

proof

seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Lm16
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by CSSPACE:3 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by VALUED_1:8
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (seqi . m) - ((seq_id (vseq . k)) . i) by A4
.= (seqi . m) - (seqi . k) by A4 ;
then |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * |.((seq_id ((vseq . m) - (vseq . k))) . i).| by VALUED_1:18
.= (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i) by VALUED_1:18 ;
then (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.((seq_id ((vseq . m) - (vseq . k))) *' ).| . i) = |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| by Lm19;
hence |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i by SEQ_1:12; :: thesis: verum

end;

A17: (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) . i <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *' ).|) by A10, A11, RSSPACE2:4;
0 <= |.((seqi . m) - (seqi . k)).| by COMPLEX1:132;
then A18: 0 <= |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| by XREAL_1:129;
A19: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| < e * e by A15, A16, A17, XXREAL_0:2;
A20: sqrt (|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) = sqrt (|.((seqi . m) - (seqi . k)).| ^2 )
.= |.((seqi . m) - (seqi . k)).| by COMPLEX1:132, SQUARE_1:89 ;
sqrt (e * e) = sqrt (e1 ^2 )
.= e by A6, SQUARE_1:89 ;
hence |.((seqi . m) - (seqi . k)).| < e by A18, A19, A20, SQUARE_1:95; :: thesis: verum

end;

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

end;

end;

hence seqi is convergent by COMSEQ_3:46; :: thesis: verum

end;

take lim seqi ; :: thesis: ( lim seqi in COMPLEX & S₁[x, lim seqi] )
thus ( lim seqi in COMPLEX & S₁[x, lim seqi] ) by A4, A5; :: thesis: verum

end;

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

A22: now

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

end;

set seqt = seq_id tseq;
A23: 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
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e * 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
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 ) )
assume A24: e1 > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 )
set e = e1 / 2;
A25: e1 / 2 > 0 by A24, XREAL_1:217;
e1 / 2 < e1 by A24, XREAL_1:218;
then A26: (e1 / 2) * (e1 / 2) < e1 * e1 by A25, XREAL_1:99;
consider k being Element of NAT such that
A27: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, A25, CLVECT_2:58;
A28: for m, n being Element of NAT st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )

proof

let m, n be Element of NAT ; :: thesis: ( n >= k & m >= k implies ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) )
assume A29: ( n >= k & m >= k ) ; :: thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A27, A29;
then A30: sqrt |.(((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))).| < e1 / 2 by CSSPACE:def 15;
A31: |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable by CSSPACE:def 11, CSSPACE:def 20;
A32: for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i
(|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i = |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| . i by COMSEQ_1:49
.= |.(((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i).| by VALUED_1:18 ;
hence 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i by COMPLEX1:132; :: thesis: verum

end;

then 0 <= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by A31, SERIES_1:21;
then A33: 0 <= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:49;
then A34: 0 <= sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) by SQUARE_1:def 4;
(seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' ) is absolutely_summable by Lm20;
then A35: (seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' ) is summable ;
for j being Element of NAT holds
( (Re ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' ))) . j >= 0 & (Im ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' ))) . j = 0 ) by Lm9;
then |.(Sum ((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' ))).| = Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *' )).| by A35, Lm8
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.((seq_id ((vseq . n) - (vseq . m))) *' ).|) by COMSEQ_1:49
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by Lm19
.= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:49 ;
then sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) < e1 / 2 by A30, Lm18;
then (sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|)) ^2 < (e1 / 2) ^2 by A34, SQUARE_1:78;
then Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| < (e1 / 2) * (e1 / 2) by A33, SQUARE_1:def 4;
hence ( |.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) by A32, COMSEQ_1:49, CSSPACE:def 11, CSSPACE:def 20; :: thesis: verum

end;

A36: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i )
A37: 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))
thus seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Lm16
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by CSSPACE: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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . $1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . $1 );
A38: S₂[ 0 ]

proof

now

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) )
assume A39: for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 )
thus ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) :: thesis: verum

proof

consider rseq0 being Complex_Sequence such that
A40: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 ) & rseq0 is convergent & tseq . 0 = lim rseq0 ) by A22;

A41: now

let m be Element of NAT ; :: thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0 )).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0 )).|
thus rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 by A39
.= (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 by SERIES_1:def 1
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 by A37
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . 0 by A37
.= (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . 0 ) * (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . 0 ) by SEQ_1:12
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ).| * (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . 0 ) by VALUED_1:18
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ).| by VALUED_1:1
.= |.(((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| * |.(((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| by VALUED_1:1
.= |.(((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))).| * |.(((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| by VALUED_1:8
.= |.(((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))).| * |.(((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))).| by VALUED_1:8
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . 0 )).| * |.(((seq_id (vseq . m)) . 0 ) - ((seq_id (vseq . n)) . 0 )).| by A40
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . 0 )).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0 )).| by A40 ; :: thesis: verum

end;

then lim rseq = |.((tseq . 0 ) - ((seq_id (vseq . n)) . 0 )).| * |.((tseq . 0 ) - ((seq_id (vseq . n)) . 0 )).| by A40, Lm23
.= |.((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| * |.((tseq . 0 ) + (- ((seq_id (vseq . n)) . 0 ))).| by VALUED_1:8
.= |.((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| * |.((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| by VALUED_1:8
.= |.((tseq + (- (seq_id (vseq . n)))) . 0 ).| * |.((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )).| by VALUED_1:1
.= |.((tseq - (seq_id (vseq . n))) . 0 ).| * |.((tseq + (- (seq_id (vseq . n)))) . 0 ).| by VALUED_1:1
.= (|.(tseq - (seq_id (vseq . n))).| . 0 ) * |.((tseq - (seq_id (vseq . n))) . 0 ).| by VALUED_1:18
.= (|.(tseq - (seq_id (vseq . n))).| . 0 ) * (|.(tseq - (seq_id (vseq . n))).| . 0 ) by VALUED_1:18
.= (|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . 0 by SEQ_1:12
.= (Partial_Sums (|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|)) . 0 by SERIES_1:def 1
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|)) . 0 by CSSPACE:3
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 by CSSPACE:3 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 ) by A40, A41, Lm23; :: thesis: verum

end;

end;

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

end;

A42: 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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) )
assume A43: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) )
assume A44: for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) )
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums (|.(seq_id ((vseq . $1) - (vseq . n))).| (#) |.(seq_id ((vseq . $1) - (vseq . n))).|)) . i;
consider rseqb being Real_Sequence such that
A45: for m being Element of NAT holds rseqb . m = H₁(m) from SEQ_1:sch 1();
A46: ( rseqb is convergent & lim rseqb = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) by A43, A45;
consider seq0 being Complex_Sequence such that
A47: ( ( for m being Element of NAT holds seq0 . m = (seq_id (vseq . m)) . (i + 1) ) & seq0 is convergent & tseq . (i + 1) = lim seq0 ) by A22;

A48: now

let m be Element of NAT ; :: thesis: rseq . m = (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m)
thus rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . (i + 1) by A44
.= ((|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i) by SERIES_1:def 1
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i) by A37
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + (rseqb . m) by A45
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . (i + 1)) + (rseqb . m) by A37
.= ((|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . (i + 1)) * (|.((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)).| * (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . (i + 1))) + (rseqb . m) by VALUED_1:18
.= (|.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).|) + (rseqb . m) by VALUED_1:18
.= (|.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).|) + (rseqb . m) by VALUED_1:1
.= (|.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (rseqb . m) by VALUED_1:1
.= (|.(((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).| * |.(((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (rseqb . m) by VALUED_1:8
.= (|.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).|) + (rseqb . m) by VALUED_1:8
.= (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m) by A47
.= (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m) by A47 ; :: thesis: verum

end;

then lim rseq = (|.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).| * |.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).|) + (lim rseqb) by A46, A47, Lm24
.= (|.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).|) + (lim rseqb) by A47, VALUED_1:8
.= (|.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (lim rseqb) by VALUED_1:8
.= (|.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).| * |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).|) + (lim rseqb) by VALUED_1:1
.= (|.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).| * |.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).|) + (lim rseqb) by VALUED_1:1
.= ((|.(tseq + (- (seq_id (vseq . n)))).| . (i + 1)) * |.((tseq + (- (seq_id (vseq . n)))) . (i + 1)).|) + (lim rseqb) by VALUED_1:18
.= ((|.(tseq - (seq_id (vseq . n))).| . (i + 1)) * (|.(tseq + (- (seq_id (vseq . n)))).| . (i + 1))) + (lim rseqb) by VALUED_1:18
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . (i + 1)) + (lim rseqb) by SEQ_1:12
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.(tseq - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by A43, A45
.= ((|.(tseq - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by CSSPACE:3
.= ((|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1)) + ((Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i) by CSSPACE:3
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) by SERIES_1:def 1 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . (i + 1) ) by A46, A47, A48, Lm24; :: 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(A38, A42);
hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) ; :: thesis: verum

end;

for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 )

proof

let n be Element of NAT ; :: thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 ) )
assume A49: n >= k ; :: thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 )
A50: for i being Element of NAT st 0 <= i holds
(Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2)

proof

let i be Element of NAT ; :: thesis: ( 0 <= i implies (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) )
assume 0 <= i ; :: thesis: (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2)
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums (|.(seq_id ((vseq . $1) - (vseq . n))).| (#) |.(seq_id ((vseq . $1) - (vseq . n))).|)) . i;
consider rseq being Real_Sequence such that
A51: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A52: rseq is convergent by A36, A51;
A53: lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i by A36, A51;
for m being Element of NAT st m >= k holds
rseq . m <= (e1 / 2) * (e1 / 2)

proof

let m be Element of NAT ; :: thesis: ( m >= k implies rseq . m <= (e1 / 2) * (e1 / 2) )
assume A54: m >= k ; :: thesis: rseq . m <= (e1 / 2) * (e1 / 2)
A55: rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i by A51;
A56: ( |.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).| is summable & Sum (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . i ) ) by A28, A49, A54;
then (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i <= Sum (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) by RSSPACE2:4;
hence rseq . m <= (e1 / 2) * (e1 / 2) by A55, A56, XXREAL_0:2; :: thesis: verum

end;

hence (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) by A52, A53, RSSPACE2:6; :: thesis: verum

end;

A57: for i being Element of NAT holds 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i
(|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i = (|.((seq_id tseq) - (seq_id (vseq . n))).| . i) * (|.((seq_id tseq) - (seq_id (vseq . n))).| . i) by SEQ_1:12;
hence 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i by XREAL_1:65; :: thesis: verum

end;

A58: Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is bounded_above

proof

now

let i be Element of NAT ; :: thesis: (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1
(Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) by A50, NAT_1:2;
hence (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1 by A26, XXREAL_0:2; :: thesis: verum

end;

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

end;

then A59: |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable by A57, SERIES_1:20;
then A60: Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is convergent by SERIES_1:def 2;
A61: Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) = lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) by SERIES_1:def 3;
lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) <= (e1 / 2) * (e1 / 2) by A50, A60, RSSPACE2:6;
then A62: Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) < e1 * e1 by A26, A61, XXREAL_0:2;
|.((seq_id tseq) - (seq_id (vseq . n))).| = |.(((seq_id tseq) - (seq_id (vseq . n))) *' ).| by Lm19;
then A63: Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' )).| < e1 * e1 by A62, COMSEQ_1:49;
|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(((seq_id tseq) - (seq_id (vseq . n))) *' ).| is summable by A59, Lm19;
then |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' )).| is summable by COMSEQ_1:49;
then ((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ) is absolutely_summable by COMSEQ_3:def 11;
then |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| <= Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' )).| by Lm7;
hence ( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 ) by A57, A58, A63, 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
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e1 * e1 ) ; :: thesis: verum

end;

A64: |.(seq_id tseq).| (#) |.(seq_id tseq).| is summable

proof

A65: for i being Element of NAT holds 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i
(|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i = (|.(seq_id tseq).| . i) * (|.(seq_id tseq).| . i) by SEQ_1:12;
hence 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i by XREAL_1:65; :: thesis: verum

end;

consider m being Element of NAT such that
A66: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < 1 * 1 ) by A23;
A67: |.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).| is summable by A66;
A68: |.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).| is summable by CSSPACE:def 11, CSSPACE:def 20;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|;
set b = |.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|;
set d = |.(seq_id tseq).| (#) |.(seq_id tseq).|;
A69: 2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) is summable by A67, SERIES_1:13;
2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) is summable by A68, SERIES_1:13;
then A70: (2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) is summable by A69, SERIES_1:10;
for i being Element of NAT holds (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i

proof

let i be Element of NAT ; :: thesis: (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i
A71: (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i = (|.(seq_id tseq).| . i) * (|.(seq_id tseq).| . i) by SEQ_1:12
.= |.((seq_id tseq) . i).| * (|.(seq_id tseq).| . i) by VALUED_1:18
.= |.((seq_id tseq) . i).| * |.((seq_id tseq) . i).| by VALUED_1:18 ;
A72: ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i = ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) . i) + ((2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) . i) by SEQ_1:11
.= (2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i)) + ((2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|)) . i) by SEQ_1:13
.= (2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i)) + (2 * ((|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) . i)) by SEQ_1:13 ;
|.((seq_id tseq) - (seq_id (vseq . m))).| . i = |.(((seq_id tseq) + (- (seq_id (vseq . m)))) . i).| by VALUED_1:18
.= |.(((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i)).| by VALUED_1:1
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then A73: (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i = |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| by SEQ_1:12;
set x = (seq_id tseq) . i;
set y = (seq_id (vseq . m)) . i;
A74: 2 * ((|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) . i) = (2 * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).|) * |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| by A73;
2 * ((|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) . i) = 2 * ((|.(seq_id (vseq . m)).| . i) * (|.(seq_id (vseq . m)).| . i)) by SEQ_1:12
.= 2 * (|.((seq_id (vseq . m)) . i).| * (|.(seq_id (vseq . m)).| . i)) by VALUED_1:18
.= 2 * (|.((seq_id (vseq . m)) . i).| * |.((seq_id (vseq . m)) . i).|) by VALUED_1:18
.= (2 * |.((seq_id (vseq . m)) . i).|) * |.((seq_id (vseq . m)) . i).| ;
hence (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i <= ((2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|)) + (2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|))) . i by A71, A72, A74, Lm22; :: thesis: verum

end;

hence |.(seq_id tseq).| (#) |.(seq_id tseq).| is summable by A65, A70, SERIES_1:24; :: thesis: verum

end;

tseq in the_set_of_ComplexSequences by CSSPACE:def 1;
then reconsider tv = tseq as Point of Complex_l2_Space by A64, CSSPACE:def 11, CSSPACE:def 20;
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 A75: 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
A76: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e * e ) by A23, A75;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A77: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
set seqvn = seq_id (vseq . n);
A78: |.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *' ))).| < e * e by A76, A77;
tseq in the_set_of_ComplexSequences by CSSPACE:def 1;
then reconsider u = tseq as VECTOR of Complex_l2_Space by A64, CSSPACE:def 11, CSSPACE:def 20;
reconsider v = vseq . n as VECTOR of Complex_l2_Space ;
seq_id (u - v) = u - v by Lm12;
then seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Lm16;
then A79: |.((u - v) .|. (u - v)).| < e * e by A78, Lm18;
0 <= Re ((u - v) .|. (u - v)) by CSSPACE:def 13;
then 0 <= |.((u - v) .|. (u - v)).| by CSSPACE:36;
then A80: sqrt |.((u - v) .|. (u - v)).| < sqrt (e ^2 ) by A79, SQUARE_1:95;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:47
.= ||.(tv - (vseq . n)).|| by CSSPACE:49
.= sqrt |.((u - v) .|. (u - v)).| by CSSPACE:def 15 ;
hence ||.((vseq . n) - tv).|| < e by A75, A80, SQUARE_1:89; :: 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 CLVECT_2:9; :: thesis: verum