let vseq be sequence of Complex_l2_Space; :: according to CLVECT_2:def 11 :: thesis: ( not vseq is Cauchy or vseq is convergent )
assume A1: vseq is Cauchy ; :: thesis: vseq is convergent
defpred S₁[ object , object ] means ex i being Nat st
( c₁ = i & ex seqi being Complex_Sequence st
( ( for n being Nat holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & c₂ = lim seqi ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in COMPLEX & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in COMPLEX & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in COMPLEX & S₁[x,y] )
then reconsider i = x as Nat ;
deffunc H₁( set ) -> set = (seq_id (vseq . c₁)) . i;
consider seqi being Complex_Sequence such that
A3: for n being Nat holds seqi . n = H₁(n) from COMSEQ_1:sch 1();
take lim seqi ; :: thesis: ( lim seqi in COMPLEX & S₁[x, lim seqi] )
thus lim seqi in COMPLEX by XCMPLX_0:def 2; :: thesis: S₁[x, lim seqi]

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

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

proof

set e1 = e;
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, CLVECT_2:58;
A6: i in NAT by ORDINAL1:def 12;

now :: thesis: for m being Nat st k <= m holds
|.((seqi . m) - (seqi . k)).| < e

set vk = vseq . k;
let m be Nat; :: thesis: ( k <= m implies |.((seqi . m) - (seqi . k)).| < e )
assume A7: k <= m ; :: thesis: |.((seqi . m) - (seqi . k)).| < e
set vm = vseq . m;
||.((vseq . m) - (vseq . k)).|| < e by A5, A7;
then A8: sqrt |.(((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))).| < e ;
set seqmk = seq_id ((vseq . m) - (vseq . k));
A9: sqrt (|.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).|) = sqrt (|.((seqi . m) - (seqi . k)).| ^2)
.= |.((seqi . m) - (seqi . k)).| by COMPLEX1:46, SQUARE_1:22 ;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Lm15
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by VALUED_1:1, A6
.= ((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 A3
.= (seqi . m) - (seqi . k) by A3 ;
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 Lm18;
then A10: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| = (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i by SEQ_1:8;
0 <= |.((seqi . m) - (seqi . k)).| by COMPLEX1:46;
then A11: 0 <= |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| ;
( (seq_id ((vseq . m) - (vseq . k))) (#) ((seq_id ((vseq . m) - (vseq . k))) *') is absolutely_summable & ( for j being 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 Lm8, Lm19;
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 Lm7
.= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) by COMSEQ_1:46 ;
then A12: sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)) < e by A8, CSSPACE:def 17;
A13: for i being Nat holds 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i

proof

let i be 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:8
.= (|.(seq_id ((vseq . m) - (vseq . k))).| . i) * (|.(seq_id ((vseq . m) - (vseq . k))).| . i) by Lm18 ;
hence 0 <= (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) . i by XREAL_1:63; :: thesis: verum

end;

|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.(seq_id ((vseq . m) - (vseq . k))).| is summable by CSSPACE:def 11;
then A14: |.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').| is summable by Lm18;
then A15: 0 <= Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) by A13, SERIES_1:18;
then 0 <= sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|)) by SQUARE_1:def 2;
then (sqrt (Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|))) ^2 < e ^2 by A12, SQUARE_1:16;
then A16: Sum (|.(seq_id ((vseq . m) - (vseq . k))).| (#) |.((seq_id ((vseq . m) - (vseq . k))) *').|) < e * e by A15, SQUARE_1:def 2;
(|.(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 A14, A13, RSSPACE2:3;
then A17: |.((seqi . m) - (seqi . k)).| * |.((seqi . m) - (seqi . k)).| < e * e by A16, A10, XXREAL_0:2;
sqrt (e * e) = sqrt (e ^2)
.= e by A4, SQUARE_1:22 ;
hence |.((seqi . m) - (seqi . k)).| < e by A11, A17, A9, SQUARE_1:27; :: thesis: verum

end;

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

end;

end;

then seqi is convergent by COMSEQ_3:46;
hence S₁[x, lim seqi] by A3; :: thesis: verum

end;

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

A19: now :: thesis: for i being Nat ex seqi being Complex_Sequence st
( ( for n being Nat holds seqi . n = (seq_id (vseq . n)) . i ) & seqi is convergent & tseq . i = lim seqi )

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

end;

A20: for e being Real st e > 0 holds
ex k being Nat st
for n being 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 Nat st
for n being 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 A21: e1 > 0 ; :: thesis: ex k being Nat st
for n being 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;
A22: e1 / 2 > 0 by A21;
then consider k being Nat such that
A23: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, CLVECT_2:58;
e1 / 2 < e1 by A21, XREAL_1:216;
then A24: (e1 / 2) * (e1 / 2) < e1 * e1 by A22, XREAL_1:97;
A25: for m, n being 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 Nat holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )

proof

let m, n be 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 Nat holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) )
assume ( 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 Nat holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) )
then ||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A23;
then A26: sqrt |.(((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))).| < e1 / 2 ;
( (seq_id ((vseq . n) - (vseq . m))) (#) ((seq_id ((vseq . n) - (vseq . m))) *') is absolutely_summable & ( for j being 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 Lm8, Lm19;
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 Lm7
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.((seq_id ((vseq . n) - (vseq . m))) *').|) by COMSEQ_1:46
.= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by Lm18
.= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:46 ;
then A27: sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) < e1 / 2 by A26, CSSPACE:def 17;
A28: for i being Nat holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i

proof

let i be 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:46
.= |.(((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:46; :: thesis: verum

end;

|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).| is summable by CSSPACE:def 11;
then 0 <= Sum (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) by A28, SERIES_1:18;
then A29: 0 <= Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| by COMSEQ_1:46;
then 0 <= sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|) by SQUARE_1:def 2;
then (sqrt (Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).|)) ^2 < (e1 / 2) ^2 by A27, SQUARE_1:16;
then Sum |.((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))).| < (e1 / 2) * (e1 / 2) by A29, SQUARE_1:def 2;
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 Nat holds 0 <= (|.(seq_id ((vseq . n) - (vseq . m))).| (#) |.(seq_id ((vseq . n) - (vseq . m))).|) . i ) ) by A28, COMSEQ_1:46, CSSPACE:def 11; :: thesis: verum

end;

A30: for n, i being Nat
for rseq being Real_Sequence st ( for m being 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 Nat; :: thesis: for i being Nat
for rseq being Real_Sequence st ( for m being 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 )
defpred S₂[ Nat] means for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . c₁ ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . c₁ );
A31: for m, k being Nat holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by Lm15;

now :: thesis: for i being Nat st ( for rseq being Real_Sequence st ( for m being 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 ) ) holds
for rseq being Real_Sequence st ( for m being 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) )

let i be Nat; :: thesis: ( ( for rseq being Real_Sequence st ( for m being 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 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 A32: for rseq being Real_Sequence st ( for m being 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 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 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

deffunc H₁( Nat) -> set = (Partial_Sums (|.(seq_id ((vseq . c₁) - (vseq . n))).| (#) |.(seq_id ((vseq . c₁) - (vseq . n))).|)) . i;
consider rseqb being Real_Sequence such that
A33: for m being Nat holds rseqb . m = H₁(m) from SEQ_1:sch 1();
consider seq0 being Complex_Sequence such that
A34: for m being Nat holds seq0 . m = (seq_id (vseq . m)) . (i + 1) and
A35: seq0 is convergent and
A36: tseq . (i + 1) = lim seq0 by A19;
let rseq be Real_Sequence; :: thesis: ( ( for m being 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 A37: for m being 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) )

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

let m be 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 A37
.= ((|.(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 A31
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1)) + (rseqb . m) by A33
.= ((|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . (i + 1)) + (rseqb . m) by A31
.= ((|.((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:8
.= (|.(((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 A34
.= (|.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| * |.((seq0 . m) - ((seq_id (vseq . n)) . (i + 1))).|) + (rseqb . m) by A34 ; :: thesis: verum

end;

A39: rseqb is convergent by A32, A33;
then lim rseq = (|.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).| * |.((lim seq0) - ((seq_id (vseq . n)) . (i + 1))).|) + (lim rseqb) by A35, A38, Lm23
.= (|.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| * |.((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).|) + (lim rseqb) by A36, 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:8
.= ((|.(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 A32, A33
.= (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 A39, A35, A38, Lm23; :: thesis: verum

end;

end;

then A40: 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 (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . 0 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 )

let rseq be Real_Sequence; :: thesis: ( ( for m being 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 A41: for m being 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
A42: for m being Nat holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A43: rseq0 is convergent and
A44: tseq . 0 = lim rseq0 by A19;

A45: now :: thesis: for m being Nat holds rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|

let m be 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 A41
.= (|.(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 A31
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| (#) |.((seq_id (vseq . m)) - (seq_id (vseq . n))).|) . 0 by A31
.= (|.((seq_id (vseq . m)) + (- (seq_id (vseq . n)))).| . 0) * (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . 0) by SEQ_1:8
.= |.(((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 A42
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| * |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| by A42 ; :: thesis: verum

end;

then lim rseq = |.((tseq . 0) - ((seq_id (vseq . n)) . 0)).| * |.((tseq . 0) - ((seq_id (vseq . n)) . 0)).| by A43, A44, Lm22
.= |.((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:8
.= (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . 0 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))).|)) . 0 ) by A43, A45, Lm22; :: thesis: verum

end;

end;

then A46: S₂[ 0 ] ;
for i being Nat holds S₂[i] from NAT_1:sch 2(A46, A40);
hence for i being Nat
for rseq being Real_Sequence st ( for m being 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 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 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 A47: 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 )
A48: for i being 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 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₁( Nat) -> set = (Partial_Sums (|.(seq_id ((vseq . c₁) - (vseq . n))).| (#) |.(seq_id ((vseq . c₁) - (vseq . n))).|)) . i;
consider rseq being Real_Sequence such that
A49: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();
A50: for m being Nat st m >= k holds
rseq . m <= (e1 / 2) * (e1 / 2)

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= (e1 / 2) * (e1 / 2) )
assume A51: m >= k ; :: thesis: rseq . m <= (e1 / 2) * (e1 / 2)
( |.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).| is summable & ( for i being Nat holds 0 <= (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) . i ) ) by A25, A47, A51;
then A52: (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:3;
A53: rseq . m = (Partial_Sums (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|)) . i by A49;
Sum (|.(seq_id ((vseq . m) - (vseq . n))).| (#) |.(seq_id ((vseq . m) - (vseq . n))).|) < (e1 / 2) * (e1 / 2) by A25, A47, A51;
hence rseq . m <= (e1 / 2) * (e1 / 2) by A53, A52, XXREAL_0:2; :: thesis: verum

end;

( rseq is convergent & lim rseq = (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i ) by A30, A49;
hence (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i <= (e1 / 2) * (e1 / 2) by A50, RSSPACE2:5; :: thesis: verum

end;

now :: thesis: for i being Nat holds (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1

let i be 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 A48;
hence (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) . i < e1 * e1 by A24, XXREAL_0:2; :: thesis: verum

end;

then A54: Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is bounded_above by SEQ_2:def 3;
A55: for i being Nat holds 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i

proof

let i be 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:8;
hence 0 <= (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) . i by XREAL_1:63; :: thesis: verum

end;

then A56: |.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).| is summable by A54, SERIES_1:17;
then Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) is convergent by SERIES_1:def 2;
then ( 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))).|)) & lim (Partial_Sums (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|)) <= (e1 / 2) * (e1 / 2) ) by A48, RSSPACE2:5, SERIES_1:def 3;
then A57: Sum (|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.((seq_id tseq) - (seq_id (vseq . n))).|) < e1 * e1 by A24, XXREAL_0:2;
|.((seq_id tseq) - (seq_id (vseq . n))).| (#) |.(((seq_id tseq) - (seq_id (vseq . n))) *').| is summable by A56, Lm18;
then |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| is summable by COMSEQ_1:46;
then ((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *') is absolutely_summable by COMSEQ_3:def 9;
then A58: |.(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 Lm6;
|.((seq_id tseq) - (seq_id (vseq . n))).| = |.(((seq_id tseq) - (seq_id (vseq . n))) *').| by Lm18;
then Sum |.(((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *')).| < e1 * e1 by A57, COMSEQ_1:46;
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 A55, A54, A58, SERIES_1:17, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Nat st
for n being 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;

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

proof

set d = |.(seq_id tseq).| (#) |.(seq_id tseq).|;
A60: for i being Nat holds 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i

proof

let i be 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:8;
hence 0 <= (|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i by XREAL_1:63; :: thesis: verum

end;

consider m being Nat such that
A61: for n being 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 A20;
set b = |.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|;
|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).| is summable by CSSPACE:def 11;
then A62: 2 (#) (|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) is summable by SERIES_1:10;
A63: for i being 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 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
A64: i in NAT by ORDINAL1:def 12;
A65: ((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:7
.= (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:9
.= (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:9 ;
set y = (seq_id (vseq . m)) . i;
set x = (seq_id tseq) . i;
A66: 2 * ((|.(seq_id (vseq . m)).| (#) |.(seq_id (vseq . m)).|) . i) = 2 * ((|.(seq_id (vseq . m)).| . i) * (|.(seq_id (vseq . m)).| . i)) by SEQ_1:8
.= 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).| ;
|.((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, A64
.= |.(((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i))).| by VALUED_1:8
.= |.(((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)).| ;
then (|.((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:8;
then A67: 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)).| ;
(|.(seq_id tseq).| (#) |.(seq_id tseq).|) . i = (|.(seq_id tseq).| . i) * (|.(seq_id tseq).| . i) by SEQ_1:8
.= |.((seq_id tseq) . i).| * (|.(seq_id tseq).| . i) by VALUED_1:18
.= |.((seq_id tseq) . i).| * |.((seq_id tseq) . i).| by VALUED_1:18 ;
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 A65, A67, A66, Lm21; :: thesis: verum

end;

|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).| is summable by A61;
then 2 (#) (|.((seq_id tseq) - (seq_id (vseq . m))).| (#) |.((seq_id tseq) - (seq_id (vseq . m))).|) is summable by SERIES_1:10;
then (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 A62, SERIES_1:7;
hence |.(seq_id tseq).| (#) |.(seq_id tseq).| is summable by A60, A63, SERIES_1:20; :: thesis: verum

end;

tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider tv = tseq as Point of Complex_l2_Space by A59, CSSPACE:def 11;
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 A68: e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Nat such that
A69: for n being 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 A20, A68;

now :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

tseq in the_set_of_ComplexSequences by FUNCT_2:8;
then reconsider u = tseq as VECTOR of Complex_l2_Space by A59, CSSPACE:def 11;
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A70: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
reconsider v = vseq . n as VECTOR of Complex_l2_Space ;
set seqvn = seq_id (vseq . n);
0 <= Re ((u - v) .|. (u - v)) by CSSPACE:def 13;
then A71: 0 <= |.((u - v) .|. (u - v)).| by CSSPACE:34;
A72: seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Lm15;
|.(Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) (((seq_id tseq) - (seq_id (vseq . n))) *'))).| < e * e by A69, A70;
then |.((u - v) .|. (u - v)).| < e * e by A72, CSSPACE:def 17;
then A73: sqrt |.((u - v) .|. (u - v)).| < sqrt (e ^2) by A71, SQUARE_1:27;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by CSSPACE:47
.= sqrt |.((u - v) .|. (u - v)).| ;
hence ||.((vseq . n) - tv).|| < e by A68, A73, SQUARE_1:22; :: thesis: verum

end;

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

end;

hence vseq is convergent by CLVECT_2:9; :: thesis: verum