:: CSSPACE3 semantic presentation

begin

definition
func the_set_of_l1ComplexSequences  ->  Subset of Linear_Space_of_ComplexSequences means :Def1: :: CSSPACE3:def 1
 for x being set holds
( x in it iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) );
existence
 ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) )
proof
defpred S1[ set ] means  seq_id $1 is absolutely_summable ;
consider IT being set  such that
A1: for x being set holds
( x in IT iff ( x in the_set_of_ComplexSequences & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in IT holds
x in the_set_of_ComplexSequences by A1;
then  IT is Subset of the_set_of_ComplexSequences by TARSKI:def_3;
hence  ex b1 being Subset of Linear_Space_of_ComplexSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) by A1, CSSPACE:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of Linear_Space_of_ComplexSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Linear_Space_of_ComplexSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) and
A3: for x being set holds
( x in X2 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) ; ::_thesis: X1 = X2
 for x being set st x in X2 holds
x in X1
proof
let x be set ; ::_thesis: ( x in X2 implies x in X1 )
assume  x in X2 ; ::_thesis: x in X1
then  ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) by A3;
hence  x in X1 by A2; ::_thesis: verum
end;
then A4: X2 c= X1 by TARSKI:def_3;
 for x being set st x in X1 holds
x in X2
proof
let x be set ; ::_thesis: ( x in X1 implies x in X2 )
assume  x in X1 ; ::_thesis: x in X2
then  ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) by A2;
hence  x in X2 by A3; ::_thesis: verum
end;
then  X1 c= X2 by TARSKI:def_3;
hence  X1 = X2 by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines the_set_of_l1ComplexSequences CSSPACE3:def_1_:_
 for b1 being Subset of Linear_Space_of_ComplexSequences holds
( b1 = the_set_of_l1ComplexSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_ComplexSequences & seq_id x is absolutely_summable ) ) );

theorem Th1: :: CSSPACE3:1
for c being Complex
for seq being Complex_Sequence
for rseq being Real_Sequence st seq is convergent & ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
proof
let c be Complex; ::_thesis: for seq being Complex_Sequence
for rseq being Real_Sequence st seq is convergent & ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
let seq be Complex_Sequence; ::_thesis: for rseq being Real_Sequence st seq is convergent & ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| )
let rseq be Real_Sequence; ::_thesis: ( seq is convergent & ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| ) )
assume that
A1: seq is convergent and
A2: for i being Element of NAT holds rseq . i = |.((seq . i) - c).| ; ::_thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| )
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def_2;
reconsider cseq = NAT --> c1 as Complex_Sequence ;
A3: for n being Element of NAT holds cseq . n = c by FUNCOP_1:7;
then A4: cseq is convergent by COMSEQ_2:9;
then reconsider seq9 = seq - cseq as convergent Complex_Sequence by A1;
 seq - cseq is convergent by A1, A4;
then A5: lim |.(seq - cseq).| = |.(lim (seq - cseq)).| by SEQ_2:27
.= |.((lim seq) - (lim cseq)).| by A1, A4, COMSEQ_2:26
.= |.((lim seq) - c).| by A3, COMSEQ_2:10 ;
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_|.(seq_-_cseq).|_._i
let i be Element of NAT ; ::_thesis: rseq . i = |.(seq - cseq).| . i
thus rseq . i = |.((seq . i) - c).| by A2
.= |.((seq . i) - (cseq . i)).| by FUNCOP_1:7
.= |.((seq . i) + (- (cseq . i))).|
.= |.((seq . i) + ((- cseq) . i)).| by VALUED_1:8
.= |.((seq - cseq) . i).| by VALUED_1:1
.= |.(seq - cseq).| . i by VALUED_1:18 ; ::_thesis: verum
end;
then A6: for x being set st x in NAT holds
rseq . x = |.(seq - cseq).| . x ;
 |.seq9.| is convergent ;
hence  ( rseq is convergent & lim rseq = |.((lim seq) - c).| ) by A6, A5, FUNCT_2:12; ::_thesis: verum
end;

registration
cluster the_set_of_l1ComplexSequences  ->  non empty ;
coherence
 not the_set_of_l1ComplexSequences is empty
proof
 seq_id CZeroseq is absolutely_summable
proof
reconsider cseq = seq_id CZeroseq as Complex_Sequence ;
 for n being Element of NAT holds cseq . n = 0c by CSSPACE:def_6;
hence  seq_id CZeroseq is absolutely_summable by COMSEQ_3:51; ::_thesis: verum
end;
hence  not the_set_of_l1ComplexSequences is empty by Def1; ::_thesis: verum
end;
end;

registration
cluster the_set_of_l1ComplexSequences  ->  linearly-closed ;
coherence
 the_set_of_l1ComplexSequences is linearly-closed
proof
set W = the_set_of_l1ComplexSequences ;
A1: for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l1ComplexSequences & u in the_set_of_l1ComplexSequences holds
v + u in the_set_of_l1ComplexSequences
proof
let v, u be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_l1ComplexSequences & u in the_set_of_l1ComplexSequences implies v + u in the_set_of_l1ComplexSequences )
assume that
A2: v in the_set_of_l1ComplexSequences and
A3: u in the_set_of_l1ComplexSequences ; ::_thesis: v + u in the_set_of_l1ComplexSequences
 seq_id (v + u) is absolutely_summable
proof
set r = |.(seq_id (v + u)).|;
set q = |.(seq_id u).|;
set p = |.(seq_id v).|;
A4: for n being Element of NAT holds 0 <= |.(seq_id (v + u)).| . n
proof
let n be Element of NAT ; ::_thesis: 0 <= |.(seq_id (v + u)).| . n
 |.(seq_id (v + u)).| . n = |.((seq_id (v + u)) . n).| by VALUED_1:18;
hence  0 <= |.(seq_id (v + u)).| . n by COMPLEX1:46; ::_thesis: verum
end;
A5: for n being Element of NAT holds |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n
A6: |.((seq_id v) . n).| + |.((seq_id u) . n).| = (|.(seq_id v).| . n) + |.((seq_id u) . n).| by VALUED_1:18
.= (|.(seq_id v).| . n) + (|.(seq_id u).| . n) by VALUED_1:18
.= (|.(seq_id v).| + |.(seq_id u).|) . n by SEQ_1:7 ;
|.(seq_id (v + u)).| . n = |.((seq_id (v + u)) . n).| by VALUED_1:18
.= |.((seq_id ((seq_id v) + (seq_id u))) . n).| by CSSPACE:2, CSSPACE:def_7
.= |.(((seq_id v) + (seq_id u)) . n).| by CSSPACE:1
.= |.(((seq_id v) . n) + ((seq_id u) . n)).| by VALUED_1:1 ;
hence  |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n by A6, COMPLEX1:56; ::_thesis: verum
end;
 seq_id u is absolutely_summable by A3, Def1;
then A7: |.(seq_id u).| is summable by COMSEQ_3:def_9;
 seq_id v is absolutely_summable by A2, Def1;
then  |.(seq_id v).| is summable by COMSEQ_3:def_9;
then  |.(seq_id v).| + |.(seq_id u).| is summable by A7, SERIES_1:7;
then  |.(seq_id (v + u)).| is summable by A4, A5, SERIES_1:20;
hence  seq_id (v + u) is absolutely_summable by COMSEQ_3:def_9; ::_thesis: verum
end;
hence  v + u in the_set_of_l1ComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum
end;
 for a being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l1ComplexSequences holds
a * v in the_set_of_l1ComplexSequences
proof
let a be Complex; ::_thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l1ComplexSequences holds
a * v in the_set_of_l1ComplexSequences
let v be VECTOR of Linear_Space_of_ComplexSequences; ::_thesis: ( v in the_set_of_l1ComplexSequences implies a * v in the_set_of_l1ComplexSequences )
assume A8: v in the_set_of_l1ComplexSequences ; ::_thesis: a * v in the_set_of_l1ComplexSequences
 seq_id (a * v) is absolutely_summable
proof
set r1 = |.a.| (#) |.(seq_id v).|;
set q1 = |.(seq_id (a * v)).|;
A9: for n being Element of NAT holds 0 <= |.(seq_id (a * v)).| . n
proof
let n be Element of NAT ; ::_thesis: 0 <= |.(seq_id (a * v)).| . n
 |.(seq_id (a * v)).| . n = |.((seq_id (a * v)) . n).| by VALUED_1:18;
hence  0 <= |.(seq_id (a * v)).| . n by COMPLEX1:46; ::_thesis: verum
end;
A10: for n being Element of NAT holds |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n
A11: a in COMPLEX by XCMPLX_0:def_2;
|.(seq_id (a * v)).| . n = |.((seq_id (a * v)) . n).| by VALUED_1:18
.= |.((seq_id (a (#) (seq_id v))) . n).| by CSSPACE:3, CSSPACE:def_7
.= |.((a (#) (seq_id v)) . n).| by CSSPACE:1
.= |.(a (#) (seq_id v)).| . n by VALUED_1:18 ;
hence  |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n by A11, COMSEQ_1:50; ::_thesis: verum
end;
 seq_id v is absolutely_summable by A8, Def1;
then  |.(seq_id v).| is summable by COMSEQ_3:def_9;
then  |.a.| (#) |.(seq_id v).| is summable by SERIES_1:10;
then  |.(seq_id (a * v)).| is summable by A9, A10, SERIES_1:20;
hence  seq_id (a * v) is absolutely_summable by COMSEQ_3:def_9; ::_thesis: verum
end;
hence  a * v in the_set_of_l1ComplexSequences by Def1, CSSPACE:def_7; ::_thesis: verum
end;
hence  the_set_of_l1ComplexSequences is linearly-closed by A1, CLVECT_1:def_7; ::_thesis: verum
end;
end;

Lm1:  CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is Subspace of Linear_Space_of_ComplexSequences
by CSSPACE:11;

registration
cluster CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is Abelian & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is add-associative & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_zeroed & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is right_complementable & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is vector-distributive & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-distributive & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-associative & CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is scalar-unital ) by CSSPACE:11;
end;

definition
func cl_norm  ->  Function of the_set_of_l1ComplexSequences,REAL means :Def2: :: CSSPACE3:def 2
 for x being set st x in the_set_of_l1ComplexSequences holds
it . x = Sum |.(seq_id x).|;
existence
 ex b1 being Function of the_set_of_l1ComplexSequences,REAL st
for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).|
proof
deffunc H1( set ) ->  Element of REAL = Sum |.(seq_id $1).|;
A1: for z being set st z in the_set_of_l1ComplexSequences holds
H1(z) in REAL ;
 ex f being Function of the_set_of_l1ComplexSequences,REAL st
for x being set st x in the_set_of_l1ComplexSequences holds
f . x = H1(x) from FUNCT_2:sch_2(A1);
hence  ex b1 being Function of the_set_of_l1ComplexSequences,REAL st
for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).| ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of the_set_of_l1ComplexSequences,REAL st ( for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).| ) & ( for x being set st x in the_set_of_l1ComplexSequences holds
b2 . x = Sum |.(seq_id x).| ) holds
b1 = b2
proof
let NORM1, NORM2 be Function of the_set_of_l1ComplexSequences,REAL; ::_thesis: ( ( for x being set st x in the_set_of_l1ComplexSequences holds
NORM1 . x = Sum |.(seq_id x).| ) & ( for x being set st x in the_set_of_l1ComplexSequences holds
NORM2 . x = Sum |.(seq_id x).| ) implies NORM1 = NORM2 )
assume that
A2: for x being set st x in the_set_of_l1ComplexSequences holds
NORM1 . x = Sum |.(seq_id x).| and
A3: for x being set st x in the_set_of_l1ComplexSequences holds
NORM2 . x = Sum |.(seq_id x).| ; ::_thesis: NORM1 = NORM2
A4: for z being set st z in the_set_of_l1ComplexSequences holds
NORM1 . z = NORM2 . z
proof
let z be set ; ::_thesis: ( z in the_set_of_l1ComplexSequences implies NORM1 . z = NORM2 . z )
assume A5: z in the_set_of_l1ComplexSequences ; ::_thesis: NORM1 . z = NORM2 . z
 NORM1 . z = Sum |.(seq_id z).| by A2, A5;
hence  NORM1 . z = NORM2 . z by A3, A5; ::_thesis: verum
end;
 ( dom NORM1 = the_set_of_l1ComplexSequences & dom NORM2 = the_set_of_l1ComplexSequences ) by FUNCT_2:def_1;
hence  NORM1 = NORM2 by A4, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines cl_norm CSSPACE3:def_2_:_
 for b1 being Function of the_set_of_l1ComplexSequences,REAL holds
( b1 = cl_norm iff for x being set st x in the_set_of_l1ComplexSequences holds
b1 . x = Sum |.(seq_id x).| );

registration
let X be non empty set ;
let Z be Element of X;
let A be BinOp of X;
let M be Function of [:COMPLEX,X:],X;
let N be Function of X,REAL;
cluster CNORMSTR(# X,Z,A,M,N #) ->  non empty ;
coherence
 not CNORMSTR(# X,Z,A,M,N #) is empty ;
end;

theorem :: CSSPACE3:2
for l being CNORMSTR st CLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is ComplexLinearSpace holds
l is ComplexLinearSpace by CSSPACE:79;

theorem Th3: :: CSSPACE3:3
for cseq being Complex_Sequence st ( for n being Element of NAT holds cseq . n = 0c ) holds
( cseq is absolutely_summable & Sum |.cseq.| = 0 )
proof
let cseq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds cseq . n = 0c ) implies ( cseq is absolutely_summable & Sum |.cseq.| = 0 ) )
assume A1: for n being Element of NAT holds cseq . n = 0c ; ::_thesis: ( cseq is absolutely_summable & Sum |.cseq.| = 0 )
A2: for n being Element of NAT holds |.cseq.| . n = 0
proof
let n be Element of NAT ; ::_thesis: |.cseq.| . n = 0
 cseq . n = 0c by A1;
hence  |.cseq.| . n = 0 by COMPLEX1:44, VALUED_1:18; ::_thesis: verum
end;
A3: for m being Element of NAT holds (Partial_Sums |.cseq.|) . m = 0
proof
defpred S1[ Element of NAT ] means |.cseq.| . $1 = (Partial_Sums |.cseq.|) . $1;
let m be Element of NAT ; ::_thesis: (Partial_Sums |.cseq.|) . m = 0
A4: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A5: |.cseq.| . k = (Partial_Sums |.cseq.|) . k ; ::_thesis: S1[k + 1]
thus |.cseq.| . (k + 1) = 0 + (|.cseq.| . (k + 1))
.= (|.cseq.| . k) + (|.cseq.| . (k + 1)) by A2
.= (Partial_Sums |.cseq.|) . (k + 1) by A5, SERIES_1:def_1 ; ::_thesis: verum
end;
A6: S1[ 0 ] by SERIES_1:def_1;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A4);
hence (Partial_Sums |.cseq.|) . m = |.cseq.| . m
.= 0 by A2 ;
::_thesis: verum
end;
A7: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums |.cseq.|) . m) - 0) < p
proof
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums |.cseq.|) . m) - 0) < p )
assume A8: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((Partial_Sums |.cseq.|) . m) - 0) < p
take  0 ; ::_thesis: for m being Element of NAT st 0 <= m holds
abs (((Partial_Sums |.cseq.|) . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs (((Partial_Sums |.cseq.|) . m) - 0) < p )
assume  0 <= m ; ::_thesis: abs (((Partial_Sums |.cseq.|) . m) - 0) < p
abs (((Partial_Sums |.cseq.|) . m) - 0) = abs (0 - 0) by A3
.= 0 by ABSVALUE:def_1 ;
hence  abs (((Partial_Sums |.cseq.|) . m) - 0) < p by A8; ::_thesis: verum
end;
then A9: Partial_Sums |.cseq.| is convergent by SEQ_2:def_6;
then A10: |.cseq.| is summable by SERIES_1:def_2;
 lim (Partial_Sums |.cseq.|) = 0 by A7, A9, SEQ_2:def_7;
hence  ( cseq is absolutely_summable & Sum |.cseq.| = 0 ) by A10, COMSEQ_3:def_9, SERIES_1:def_3; ::_thesis: verum
end;

theorem Th4: :: CSSPACE3:4
for cseq being Complex_Sequence st cseq is absolutely_summable & Sum |.cseq.| = 0 holds
for n being Element of NAT holds cseq . n = 0c
proof
let cseq be Complex_Sequence; ::_thesis: ( cseq is absolutely_summable & Sum |.cseq.| = 0 implies for n being Element of NAT holds cseq . n = 0c )
assume that
A1: cseq is absolutely_summable and
A2: Sum |.cseq.| = 0 ; ::_thesis: for n being Element of NAT holds cseq . n = 0c
reconsider rseq = |.cseq.| as Real_Sequence ;
A3: for n being Element of NAT holds 0 <= |.cseq.| . n
proof
let n be Element of NAT ; ::_thesis: 0 <= |.cseq.| . n
 0 <= |.(cseq . n).| by COMPLEX1:46;
hence  0 <= |.cseq.| . n by VALUED_1:18; ::_thesis: verum
end;
A4: rseq is summable by A1, COMSEQ_3:def_9;
 for n being Element of NAT holds cseq . n = 0c
proof
let n be Element of NAT ; ::_thesis: cseq . n = 0c
 |.cseq.| . n = 0 by A2, A4, A3, RSSPACE:17;
then  |.(cseq . n).| = 0 by VALUED_1:18;
hence  cseq . n = 0c by COMPLEX1:45; ::_thesis: verum
end;
hence  for n being Element of NAT holds cseq . n = 0c ; ::_thesis: verum
end;

Lm2:  CLSStruct(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)) #) is ComplexLinearSpace
;

definition
func Complex_l1_Space  ->  non empty CNORMSTR  equals :: CSSPACE3:def 3
 CNORMSTR(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),cl_norm #);
coherence
 CNORMSTR(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),cl_norm #) is non empty CNORMSTR ;
end;

:: deftheorem  defines Complex_l1_Space CSSPACE3:def_3_:_
 Complex_l1_Space = CNORMSTR(# the_set_of_l1ComplexSequences,(Zero_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l1ComplexSequences,Linear_Space_of_ComplexSequences)),cl_norm #);

theorem Th5: :: CSSPACE3:5
Complex_l1_Space is ComplexLinearSpace by Lm2, CSSPACE:79;

begin

theorem Th6: :: CSSPACE3:6
( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x being set holds
( x is VECTOR of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) ) & 0. Complex_l1_Space = CZeroseq & ( for u being VECTOR of Complex_l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u) ) & ( for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| ) )
proof
set l1 = Complex_l1_Space ;
A1: for x being set holds
( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) )
proof
let x be set ; ::_thesis: ( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) )
 ( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by CSSPACE:def_1;
hence  ( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) by Def1; ::_thesis: verum
end;
A2: for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v)
proof
let u, v be VECTOR of Complex_l1_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_l1ComplexSequences ;
 dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A3: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l1ComplexSequences) = [:the_set_of_l1ComplexSequences,the_set_of_l1ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l1ComplexSequences) . [u,v] by CSSPACE:def_8
.= u1 + v1 by A3, FUNCT_1:47 ;
hence  u + v = (seq_id u) + (seq_id v) by CSSPACE:2, CSSPACE:def_7; ::_thesis: verum
end;
A4: for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u)
proof
let p be Complex; ::_thesis: for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u)
let u be VECTOR of Complex_l1_Space; ::_thesis: p * u = p (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_l1ComplexSequences ;
 dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def_1;
then A5: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l1ComplexSequences:]) = [:COMPLEX,the_set_of_l1ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
reconsider p = p as Element of COMPLEX by XCMPLX_0:def_2;
p * u = the Mult of Complex_l1_Space . [p,u] by CLVECT_1:def_1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l1ComplexSequences:]) . [p,u] by CSSPACE:def_9
.= the Mult of Linear_Space_of_ComplexSequences . [p,u] by A5, FUNCT_1:47
.= p * u1 by CLVECT_1:def_1 ;
hence  p * u = p (#) (seq_id u) by CSSPACE:3, CSSPACE:def_7; ::_thesis: verum
end;
A6: for u being VECTOR of Complex_l1_Space holds u = seq_id u
proof
let u be VECTOR of Complex_l1_Space; ::_thesis: u = seq_id u
 u is VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
hence  u = seq_id u by CSSPACE:def_2, CSSPACE:def_7; ::_thesis: verum
end;
A7: for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of Complex_l1_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r) * u by Th5, CLVECT_1:3
.= (- 1r) (#) (seq_id u) by A4
.= - (seq_id u) by COMSEQ_1:11 ;
hence  ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A6; ::_thesis: verum
end;
A8: for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of Complex_l1_Space; ::_thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A2
.= (seq_id u) - (seq_id v) by A7 ; ::_thesis: verum
end;
A9: for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| by Def2;
0. Complex_l1_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def_10
.= CZeroseq by CSSPACE:def_7 ;
hence  ( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x being set holds
( x is VECTOR of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) ) & 0. Complex_l1_Space = CZeroseq & ( for u being VECTOR of Complex_l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u) ) & ( for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| ) ) by A1, A6, A2, A4, A7, A8, A9; ::_thesis: verum
end;

theorem Th7: :: CSSPACE3:7
for x, y being Point of Complex_l1_Space
for p being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
proof
let x, y be Point of Complex_l1_Space; ::_thesis: for p being Complex holds
( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
let p be Complex; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| )
A1: for n being Element of NAT holds 0 <= |.(seq_id x).| . n
proof
let n be Element of NAT ; ::_thesis: 0 <= |.(seq_id x).| . n
 0 <= |.((seq_id x) . n).| by COMPLEX1:46;
hence  0 <= |.(seq_id x).| . n by VALUED_1:18; ::_thesis: verum
end;
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_|.(seq_id_(x_+_y)).|_._n
let n be Element of NAT ; ::_thesis: 0 <= |.(seq_id (x + y)).| . n
 |.(seq_id (x + y)).| . n = |.((seq_id (x + y)) . n).| by VALUED_1:18;
hence  0 <= |.(seq_id (x + y)).| . n by COMPLEX1:46; ::_thesis: verum
end;
A3: for n being Element of NAT holds |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).|
|.(seq_id (x + y)).| . n = |.(seq_id ((seq_id x) + (seq_id y))).| . n by Th6
.= |.((seq_id x) + (seq_id y)).| . n by CSSPACE:1
.= |.(((seq_id x) + (seq_id y)) . n).| by VALUED_1:18
.= |.(((seq_id x) . n) + ((seq_id y) . n)).| by VALUED_1:1 ;
hence  |.(seq_id (x + y)).| . n = |.(((seq_id x) . n) + ((seq_id y) . n)).| ; ::_thesis: verum
end;
A4: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n)
 |.(((seq_id x) . n) + ((seq_id y) . n)).| <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by COMPLEX1:56;
then  |.(seq_id (x + y)).| . n <= |.((seq_id x) . n).| + |.((seq_id y) . n).| by A3;
then  |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + |.((seq_id y) . n).| by VALUED_1:18;
hence  |.(seq_id (x + y)).| . n <= (|.(seq_id x).| . n) + (|.(seq_id y).| . n) by VALUED_1:18; ::_thesis: verum
end;
A5: for n being Element of NAT holds |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
proof
let n be Element of NAT ; ::_thesis: |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n
 (|.(seq_id x).| . n) + (|.(seq_id y).| . n) = (|.(seq_id x).| + |.(seq_id y).|) . n by SEQ_1:7;
hence  |.(seq_id (x + y)).| . n <= (|.(seq_id x).| + |.(seq_id y).|) . n by A4; ::_thesis: verum
end;
 seq_id y is absolutely_summable by Def1;
then A6: |.(seq_id y).| is summable by COMSEQ_3:def_9;
 seq_id x is absolutely_summable by Def1;
then  |.(seq_id x).| is summable by COMSEQ_3:def_9;
then  |.(seq_id x).| + |.(seq_id y).| is summable by A6, SERIES_1:7;
then A7: Sum |.(seq_id (x + y)).| <= Sum (|.(seq_id x).| + |.(seq_id y).|) by A5, A2, SERIES_1:20;
A8: now__::_thesis:_(_x_=_0._Complex_l1_Space_implies_||.x.||_=_0_)
assume  x = 0. Complex_l1_Space ; ::_thesis: ||.x.|| = 0
then A9: for n being Element of NAT holds (seq_id x) . n = 0 by Th6, CSSPACE:def_6;
thus ||.x.|| = the normF of Complex_l1_Space . x
.= Sum |.(seq_id x).| by Def2
.= 0 by A9, Th3 ; ::_thesis: verum
end;
A10: Sum |.(seq_id (x + y)).| = ||.(x + y).|| by Th6;
A11: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._Complex_l1_Space_)
A12: x in the_set_of_ComplexSequences by Def1;
assume A13: ||.x.|| = 0 ; ::_thesis: x = 0. Complex_l1_Space
 ( ||.x.|| = Sum |.(seq_id x).| & seq_id x is absolutely_summable ) by Th6;
then  for n being Element of NAT holds 0 = (seq_id x) . n by A13, Th4;
hence  x = 0. Complex_l1_Space by A12, Th6, CSSPACE:def_6; ::_thesis: verum
end;
A14: ( ||.x.|| = Sum |.(seq_id x).| & ||.y.|| = Sum |.(seq_id y).| ) by Th6;
A15: for n being Element of NAT holds |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n)
proof
let n be Element of NAT ; ::_thesis: |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n)
reconsider p = p as Element of COMPLEX by XCMPLX_0:def_2;
|.(p (#) (seq_id x)).| . n = |.((p (#) (seq_id x)) . n).| by VALUED_1:18
.= |.(p * ((seq_id x) . n)).| by VALUED_1:6
.= |.p.| * |.((seq_id x) . n).| by COMPLEX1:65
.= |.p.| * (|.(seq_id x).| . n) by VALUED_1:18 ;
hence  |.(p (#) (seq_id x)).| . n = |.p.| * (|.(seq_id x).| . n) ; ::_thesis: verum
end;
 seq_id x is absolutely_summable by Def1;
then A16: |.(seq_id x).| is summable by COMSEQ_3:def_9;
 seq_id x is absolutely_summable by Def1;
then A17: |.(seq_id x).| is summable by COMSEQ_3:def_9;
||.(p * x).|| = Sum |.(seq_id (p * x)).| by Th6
.= Sum |.(seq_id (p (#) (seq_id x))).| by Th6
.= Sum |.(p (#) (seq_id x)).| by CSSPACE:1
.= Sum (|.p.| (#) |.(seq_id x).|) by A15, SEQ_1:9
.= |.p.| * (Sum |.(seq_id x).|) by A16, SERIES_1:10
.= |.p.| * ||.x.|| by Th6 ;
hence  ( ( ||.x.|| = 0 implies x = 0. Complex_l1_Space ) & ( x = 0. Complex_l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(p * x).|| = |.p.| * ||.x.|| ) by A11, A8, A1, A17, A14, A10, A6, A7, SERIES_1:7, SERIES_1:18; ::_thesis: verum
end;

registration
cluster Complex_l1_Space  ->  non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like ;
coherence
 ( Complex_l1_Space is reflexive & Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable )
proof
thus  Complex_l1_Space is reflexive ::_thesis: ( Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable )
proof
thus  ||.(0. Complex_l1_Space).|| = 0 by Th7; :: according to NORMSP_0:def_6 ::_thesis: verum
end;
thus  ( Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable ) by Lm2, Th7, CLVECT_1:def_13, CSSPACE:79, NORMSP_0:def_5; ::_thesis: verum
end;
end;

Lm3:  for c being Complex
for seq being Complex_Sequence
for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
proof
let c be Complex; ::_thesis: for seq being Complex_Sequence
for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
let seq be Complex_Sequence; ::_thesis: for seq1 being Real_Sequence st seq is convergent & seq1 is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
let seq1 be Real_Sequence; ::_thesis: ( seq is convergent & seq1 is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) )
assume that
A1: seq is convergent and
A2: seq1 is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) holds
( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
reconsider c1 = c as Element of COMPLEX by XCMPLX_0:def_2;
reconsider cseq = NAT --> c1 as Complex_Sequence ;
A3: for n being Element of NAT holds cseq . n = c by FUNCOP_1:7;
then A4: lim cseq = c by COMSEQ_2:10
.= cseq . 0 by FUNCOP_1:7 ;
A5: cseq is convergent by A3, COMSEQ_2:9;
then  seq - cseq is convergent by A1;
then A6: lim |.(seq - cseq).| = |.(lim (seq - cseq)).| by SEQ_2:27
.= |.((lim seq) - (cseq . 0)).| by A1, A4, A5, COMSEQ_2:26
.= |.((lim seq) - c).| by FUNCOP_1:7 ;
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ) implies ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) )
assume A7: for i being Element of NAT holds rseq . i = |.((seq . i) - c).| + (seq1 . i) ; ::_thesis: ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) )
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_(|.(seq_-_cseq).|_+_seq1)_._i
let i be Element of NAT ; ::_thesis: rseq . i = (|.(seq - cseq).| + seq1) . i
thus rseq . i = |.((seq . i) - c).| + (seq1 . i) by A7
.= |.((seq . i) - (cseq . i)).| + (seq1 . i) by FUNCOP_1:7
.= |.((seq . i) + (- (cseq . i))).| + (seq1 . i)
.= |.((seq . i) + ((- cseq) . i)).| + (seq1 . i) by VALUED_1:8
.= |.((seq - cseq) . i).| + (seq1 . i) by VALUED_1:1
.= (|.(seq - cseq).| . i) + (seq1 . i) by VALUED_1:18
.= (|.(seq - cseq).| + seq1) . i by SEQ_1:7 ; ::_thesis: verum
end;
then A8: rseq = |.(seq - cseq).| + seq1 by FUNCT_2:63;
reconsider seq1 = seq - cseq as convergent Complex_Sequence by A1, A5;
 |.seq1.| is convergent ;
hence  ( rseq is convergent & lim rseq = |.((lim seq) - c).| + (lim seq1) ) by A2, A8, A6, SEQ_2:6; ::_thesis: verum
end;

definition
let X be non empty CNORMSTR ;
let x, y be Point of X;
func dist (x,y) ->  Real equals :: CSSPACE3:def 4
||.(x - y).||;
coherence
 ||.(x - y).|| is Real ;
end;

:: deftheorem  defines dist CSSPACE3:def_4_:_
 for X being non empty CNORMSTR
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;

definition
let CNRM be non empty CNORMSTR ;
let seqt be sequence of CNRM;
attrseqt is CCauchy  means :Def5: :: CSSPACE3:def 5
 for r1 being Real st r1 > 0 holds
ex k1 being Element of NAT st
for n1, m1 being Element of NAT st n1 >= k1 & m1 >= k1 holds
dist ((seqt . n1),(seqt . m1)) < r1;
end;

:: deftheorem Def5 defines CCauchy CSSPACE3:def_5_:_
 for CNRM being non empty CNORMSTR
for seqt being sequence of CNRM holds
( seqt is CCauchy iff for r1 being Real st r1 > 0 holds
ex k1 being Element of NAT st
for n1, m1 being Element of NAT st n1 >= k1 & m1 >= k1 holds
dist ((seqt . n1),(seqt . m1)) < r1 );

notation
let CNRM be non empty CNORMSTR ;
let seq be sequence of CNRM;
synonym  Cauchy_sequence_by_Norm seq for  CCauchy ;
end;


theorem Th8: :: CSSPACE3:8
for NRM being ComplexNormSpace
for seq being sequence of NRM holds
( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proof
let NRM be ComplexNormSpace; ::_thesis: for seq being sequence of NRM holds
( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
let seq be sequence of NRM; ::_thesis: ( seq is Cauchy_sequence_by_Norm iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
thus  ( seq is Cauchy_sequence_by_Norm implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) ::_thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy_sequence_by_Norm )
proof
assume A1: seq is Cauchy_sequence_by_Norm ; ::_thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
assume  r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
then consider k being Element of NAT  such that
A2: for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r by A1, Def5;
 for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
proof
let n, m be Element of NAT ; ::_thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < r )
assume  ( n >= k & m >= k ) ; ::_thesis: ||.((seq . n) - (seq . m)).|| < r
then  dist ((seq . n),(seq . m)) < r by A2;
hence  ||.((seq . n) - (seq . m)).|| < r ; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; ::_thesis: verum
end;
thus  ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy_sequence_by_Norm ) ::_thesis: verum
proof
assume A3: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; ::_thesis: seq is Cauchy_sequence_by_Norm
now__::_thesis:_for_r_being_Real_st_r_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
dist_((seq_._n),(seq_._m))_<_r
let r be Real; ::_thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume A4: r > 0 ; ::_thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
now__::_thesis:_ex_k_being_Element_of_NAT_st_
for_n,_m_being_Element_of_NAT_st_n_>=_k_&_m_>=_k_holds_
dist_((seq_._n),(seq_._m))_<_r
consider k being Element of NAT  such that
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A3, A4;
 for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r by A5;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r ; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r ; ::_thesis: verum
end;
hence  seq is Cauchy_sequence_by_Norm by Def5; ::_thesis: verum
end;
end;

theorem :: CSSPACE3:9
for vseq being sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent
proof
let vseq be sequence of Complex_l1_Space; ::_thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: vseq is Cauchy_sequence_by_Norm ; ::_thesis: vseq is convergent
defpred S1[ set , set ] means  ex i being Element of NAT st
( $1 = i & ex rseqi being Complex_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 COMPLEX & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in NAT implies ex y being set st
( y in COMPLEX & S1[x,y] ) )
assume  x in NAT ; ::_thesis: ex y being set st
( y in COMPLEX & S1[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H1( Element of NAT ) ->  Element of COMPLEX = (seq_id (vseq . $1)) . i;
consider rseqi being Complex_Sequence such that
A3: for n being Element of NAT holds rseqi . n = H1(n) from COMSEQ_1:sch_1();
take  lim rseqi ; ::_thesis: ( lim rseqi in COMPLEX & S1[x, lim rseqi] )
now__::_thesis:_for_e_being_Real_st_e_>_0_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
|.((rseqi_._m)_-_(rseqi_._k)).|_<_e
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
|.((rseqi . m) - (rseqi . k)).| < e )
assume A4: e > 0 ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
thus  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e ::_thesis: verum
proof
consider k being Element of NAT  such that
A5: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, Th8;
 for m being Element of NAT st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
proof
let m be Element of NAT ; ::_thesis: ( k <= m implies |.((rseqi . m) - (rseqi . k)).| < e )
assume A6: k <= m ; ::_thesis: |.((rseqi . m) - (rseqi . k)).| < e
A7: for i being Element of NAT holds 0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i
proof
let i be Element of NAT ; ::_thesis: 0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i
 0 <= |.((seq_id ((vseq . m) - (vseq . k))) . i).| by COMPLEX1:46;
hence  0 <= |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18; ::_thesis: verum
end;
 seq_id ((vseq . m) - (vseq . k)) is absolutely_summable by Def1;
then  |.(seq_id ((vseq . m) - (vseq . k))).| is summable by COMSEQ_3:def_9;
then A8: |.(seq_id ((vseq . m) - (vseq . k))).| . i <= Sum |.(seq_id ((vseq . m) - (vseq . k))).| by A7, RSSPACE2:3;
seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th6
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by CSSPACE:1 ;
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)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then A9: |.((rseqi . m) - (rseqi . k)).| = |.(seq_id ((vseq . m) - (vseq . k))).| . i by VALUED_1:18;
 ||.((vseq . m) - (vseq . k)).|| = Sum |.(seq_id ((vseq . m) - (vseq . k))).| by Th6;
then  Sum |.(seq_id ((vseq . m) - (vseq . k))).| < e by A5, A6;
hence  |.((rseqi . m) - (rseqi . k)).| < e by A8, A9, XXREAL_0:2; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e ; ::_thesis: verum
end;
end;
then  rseqi is convergent by COMSEQ_3:46;
hence  ( lim rseqi in COMPLEX & S1[x, lim rseqi] ) by A3; ::_thesis: verum
end;
consider f being Function of NAT,COMPLEX such that
A10: for x being set st x in NAT holds
S1[x,f . x] from FUNCT_2:sch_1(A2);
reconsider tseq = f as Complex_Sequence ;
A11: now__::_thesis:_for_i_being_Element_of_NAT_ex_rseqi_being_Complex_Sequence_st_
(_(_for_n_being_Element_of_NAT_holds_rseqi_._n_=_(seq_id_(vseq_._n))_._i_)_&_rseqi_is_convergent_&_tseq_._i_=_lim_rseqi_)
let i be Element of NAT ; ::_thesis: ex rseqi being Complex_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 Complex_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A10;
hence  ex rseqi being Complex_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;
A12: 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))).| is summable & Sum |.((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
( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 ) )
assume A13: 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))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 )
set e = e1 / 2;
A14: e1 / 2 < e1 by A13, XREAL_1:216;
 e1 / 2 > 0 by A13, XREAL_1:215;
then consider k being Element of NAT  such that
A15: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, Th8;
A16: for m, n being Element of NAT st n >= k & m >= k holds
( |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum |.(seq_id ((vseq . n) - (vseq . m))).| < e1 / 2 & ( for i being Element of NAT holds 0 <= |.(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))).| is summable & Sum |.(seq_id ((vseq . n) - (vseq . m))).| < e1 / 2 & ( for i being Element of NAT holds 0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i ) ) )
assume  ( n >= k & m >= k ) ; ::_thesis: ( |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum |.(seq_id ((vseq . n) - (vseq . m))).| < e1 / 2 & ( for i being Element of NAT holds 0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i ) )
then  ||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A15;
then A17: the normF of Complex_l1_Space . ((vseq . n) - (vseq . m)) < e1 / 2 ;
A18: for i being Element of NAT holds 0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i
proof
let i be Element of NAT ; ::_thesis: 0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i
 0 <= |.((seq_id ((vseq . n) - (vseq . m))) . i).| by COMPLEX1:46;
hence  0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i by VALUED_1:18; ::_thesis: verum
end;
 seq_id ((vseq . n) - (vseq . m)) is absolutely_summable by Def1;
hence  ( |.(seq_id ((vseq . n) - (vseq . m))).| is summable & Sum |.(seq_id ((vseq . n) - (vseq . m))).| < e1 / 2 & ( for i being Element of NAT holds 0 <= |.(seq_id ((vseq . n) - (vseq . m))).| . i ) ) by A17, A18, Def2, COMSEQ_3:def_9; ::_thesis: verum
end;
A19: 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))).|) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((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))).|) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i )
defpred S2[ 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))).|) . $1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . $1 );
A20: 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 Th6;
hence  seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by CSSPACE:1; ::_thesis: verum
end;
now__::_thesis:_for_i_being_Element_of_NAT_st_(_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|)_._i_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|)_._i_)_)_holds_
for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|)_._(i_+_1)_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|)_._(i_+_1)_)
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))).|) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((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))).|) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1) ) )
assume A21: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((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))).|) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((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))).|) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1) ) ::_thesis: verum
proof
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums |.(seq_id ((vseq . $1) - (vseq . n))).|) . i;
consider rseqb being Real_Sequence such that
A22: for m being Element of NAT holds rseqb . m = H1(m) from SEQ_1:sch_1();
consider rseq0 being Complex_Sequence such that
A23: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A24: rseq0 is convergent and
A25: tseq . (i + 1) = lim rseq0 by A11;
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1) ) )
assume A26: for m being Element of NAT holds rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1) ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . (i + 1) )
A27: now__::_thesis:_for_m_being_Element_of_NAT_holds_rseq_._m_=_|.((rseq0_._m)_-_((seq_id_(vseq_._n))_._(i_+_1))).|_+_(rseqb_._m)
let m be Element of NAT ; ::_thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)
thus rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . (i + 1) by A26
.= (|.(seq_id ((vseq . m) - (vseq . n))).| . (i + 1)) + ((Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . i) by SERIES_1:def_1
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . (i + 1)) + ((Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . i) by A20
.= (|.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . (i + 1)) + (rseqb . m) by A22
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)).| + (rseqb . m) by VALUED_1:18
.= |.(((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)))).| + (rseqb . m) by VALUED_1:8
.= |.(((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m)
.= |.((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))).| + (rseqb . m) by A23 ; ::_thesis: verum
end;
A28: rseqb is convergent by A21, A22;
then  lim rseq = |.((lim rseq0) - ((seq_id (vseq . n)) . (i + 1))).| + (lim rseqb) by A24, A27, Lm3
.= |.((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))).| + (lim rseqb) by A25
.= |.((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))).| + (lim rseqb) by VALUED_1:8
.= |.((tseq - (seq_id (vseq . n))) . (i + 1)).| + (lim rseqb) by VALUED_1:1
.= (|.(tseq - (seq_id (vseq . n))).| . (i + 1)) + (lim rseqb) by VALUED_1:18
.= (|.(tseq - (seq_id (vseq . n))).| . (i + 1)) + ((Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i) by A21, A22
.= (|.((seq_id tseq) - (seq_id (vseq . n))).| . (i + 1)) + ((Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i) by CSSPACE:1
.= (Partial_Sums |.((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))).|) . (i + 1) ) by A28, A24, A27, Lm3; ::_thesis: verum
end;
end;
then A29: for i being Element of NAT st S2[i] holds
S2[i + 1] ;
now__::_thesis:_for_rseq_being_Real_Sequence_st_(_for_m_being_Element_of_NAT_holds_rseq_._m_=_(Partial_Sums_|.(seq_id_((vseq_._m)_-_(vseq_._n))).|)_._0_)_holds_
(_rseq_is_convergent_&_lim_rseq_=_(Partial_Sums_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|)_._0_)
let rseq be Real_Sequence; ::_thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . 0 ) )
assume A30: for m being Element of NAT holds rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 ; ::_thesis: ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . 0 )
thus  ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . 0 ) ::_thesis: verum
proof
consider rseq0 being Complex_Sequence such that
A31: for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A32: rseq0 is convergent and
A33: tseq . 0 = lim rseq0 by A11;
A34: for m being Element of NAT holds rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|
proof
let m be Element of NAT ; ::_thesis: rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).|
rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . 0 by A30
.= |.(seq_id ((vseq . m) - (vseq . n))).| . 0 by SERIES_1:def_1
.= |.((seq_id (vseq . m)) - (seq_id (vseq . n))).| . 0 by A20
.= |.(((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0).| by VALUED_1:18
.= |.(((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:1
.= |.(((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))).| by VALUED_1:8
.= |.(((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)).| ;
hence  rseq . m = |.((rseq0 . m) - ((seq_id (vseq . n)) . 0)).| by A31; ::_thesis: verum
end;
then  lim rseq = |.((lim rseq0) - ((seq_id (vseq . n)) . 0)).| by A32, Th1
.= |.((tseq . 0) + (- ((seq_id (vseq . n)) . 0))).| by A33
.= |.((tseq . 0) + ((- (seq_id (vseq . n))) . 0)).| by VALUED_1:8
.= |.((tseq - (seq_id (vseq . n))) . 0).| by VALUED_1:1
.= |.(((seq_id tseq) - (seq_id (vseq . n))) . 0).| by CSSPACE:1
.= |.((seq_id tseq) - (seq_id (vseq . n))).| . 0 by VALUED_1:18
.= (Partial_Sums |.((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))).|) . 0 ) by A32, A34, Th1; ::_thesis: verum
end;
end;
then A35: S2[ 0 ] ;
 for i being Element of NAT holds S2[i] from NAT_1:sch_1(A35, 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 |.(seq_id ((vseq . m) - (vseq . n))).|) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums |.((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))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 )
proof
let n be Element of NAT ; ::_thesis: ( n >= k implies ( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 ) )
assume A36: n >= k ; ::_thesis: ( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 )
A37: for i being Element of NAT st 0 <= i holds
(Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i <= e1 / 2
proof
let i be Element of NAT ; ::_thesis: ( 0 <= i implies (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i <= e1 / 2 )
assume  0 <= i ; ::_thesis: (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i <= e1 / 2
deffunc H1( Element of NAT ) ->  Element of REAL = (Partial_Sums |.(seq_id ((vseq . $1) - (vseq . n))).|) . i;
consider rseq being Real_Sequence such that
A38: for m being Element of NAT holds rseq . m = H1(m) from SEQ_1:sch_1();
A39: 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 )
A40: rseq . m = (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . i by A38;
assume A41: m >= k ; ::_thesis: rseq . m <= e1 / 2
then  ( |.(seq_id ((vseq . m) - (vseq . n))).| is summable & ( for i being Element of NAT holds 0 <= |.(seq_id ((vseq . m) - (vseq . n))).| . i ) ) by A16, A36;
then A42: (Partial_Sums |.(seq_id ((vseq . m) - (vseq . n))).|) . i <= Sum |.(seq_id ((vseq . m) - (vseq . n))).| by RSSPACE2:3;
 Sum |.(seq_id ((vseq . m) - (vseq . n))).| < e1 / 2 by A16, A36, A41;
hence  rseq . m <= e1 / 2 by A42, A40, XXREAL_0:2; ::_thesis: verum
end;
 ( rseq is convergent & lim rseq = (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i ) by A19, A38;
hence  (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i <= e1 / 2 by A39, RSSPACE2:5; ::_thesis: verum
end;
now__::_thesis:_ex_e1_being_Real_st_
for_i_being_Element_of_NAT_holds_(Partial_Sums_|.((seq_id_tseq)_-_(seq_id_(vseq_._n))).|)_._i_<_e1
take e1 = e1; ::_thesis: for i being Element of NAT holds (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i < e1
let i be Element of NAT ; ::_thesis: (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i < e1
 (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i <= e1 / 2 by A37, NAT_1:2;
hence  (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) . i < e1 by A14, XXREAL_0:2; ::_thesis: verum
end;
then A43: Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).| is bounded_above by SEQ_2:def_3;
A44: for i being Element of NAT holds 0 <= |.((seq_id tseq) - (seq_id (vseq . n))).| . i
proof
let i be Element of NAT ; ::_thesis: 0 <= |.((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 VALUED_1:18;
hence  0 <= |.((seq_id tseq) - (seq_id (vseq . n))).| . i by COMPLEX1:46; ::_thesis: verum
end;
then  |.((seq_id tseq) - (seq_id (vseq . n))).| is summable by A43, SERIES_1:17;
then  Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).| is convergent by SERIES_1:def_2;
then  ( Sum |.((seq_id tseq) - (seq_id (vseq . n))).| = lim (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) & lim (Partial_Sums |.((seq_id tseq) - (seq_id (vseq . n))).|) <= e1 / 2 ) by A37, RSSPACE2:5, SERIES_1:def_3;
hence  ( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 ) by A14, A44, A43, SERIES_1:17, XXREAL_0:2; ::_thesis: verum
end;
hence  ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e1 ) ; ::_thesis: verum
end;
 |.(seq_id tseq).| is summable
proof
set d = |.(seq_id tseq).|;
A45: for i being Element of NAT holds 0 <= |.(seq_id tseq).| . i
proof
let i be Element of NAT ; ::_thesis: 0 <= |.(seq_id tseq).| . i
 |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| by VALUED_1:18;
hence  0 <= |.(seq_id tseq).| . i by COMPLEX1:46; ::_thesis: verum
end;
consider m being Element of NAT  such that
A46: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < 1 ) by A12;
set b = |.(seq_id (vseq . m)).|;
set a = |.((seq_id tseq) - (seq_id (vseq . m))).|;
 seq_id (vseq . m) is absolutely_summable by Def1;
then A47: |.(seq_id (vseq . m)).| is summable by COMSEQ_3:def_9;
A48: for i being Element of NAT holds |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i
proof
let i be Element of NAT ; ::_thesis: |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i
A49: ( |.(seq_id (vseq . m)).| . i = |.((seq_id (vseq . m)) . i).| & |.(seq_id tseq).| . i = |.((seq_id tseq) . i).| ) by VALUED_1:18;
|.((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  (|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i) <= |.((seq_id tseq) - (seq_id (vseq . m))).| . i by A49, COMPLEX1:59;
then  ((|.(seq_id tseq).| . i) - (|.(seq_id (vseq . m)).| . i)) + (|.(seq_id (vseq . m)).| . i) <= (|.((seq_id tseq) - (seq_id (vseq . m))).| . i) + (|.(seq_id (vseq . m)).| . i) by XREAL_1:6;
hence  |.(seq_id tseq).| . i <= (|.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).|) . i by SEQ_1:7; ::_thesis: verum
end;
 |.((seq_id tseq) - (seq_id (vseq . m))).| is summable by A46;
then  |.((seq_id tseq) - (seq_id (vseq . m))).| + |.(seq_id (vseq . m)).| is summable by A47, SERIES_1:7;
hence  |.(seq_id tseq).| is summable by A45, A48, SERIES_1:20; ::_thesis: verum
end;
then A50: seq_id tseq is absolutely_summable by COMSEQ_3:def_9;
A51: tseq in the_set_of_ComplexSequences by CSSPACE:def_1;
then reconsider tv = tseq as Point of Complex_l1_Space by A50, 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  e > 0 ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
then consider m being Element of NAT  such that
A52: for n being Element of NAT st n >= m holds
( |.((seq_id tseq) - (seq_id (vseq . n))).| is summable & Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e ) by A12;
now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_
||.((vseq_._n)_-_tv).||_<_e
reconsider u = tseq as VECTOR of Complex_l1_Space by A50, A51, Def1;
let n be Element of NAT ; ::_thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume  n >= m ; ::_thesis: ||.((vseq . n) - tv).|| < e
then A53: Sum |.((seq_id tseq) - (seq_id (vseq . n))).| < e by A52;
reconsider v = vseq . n as VECTOR of Complex_l1_Space ;
 seq_id (u - v) = u - v by Th6;
then  Sum |.(seq_id (u - v)).| = Sum |.((seq_id tseq) - (seq_id (vseq . n))).| by Th6;
then A54: the normF of Complex_l1_Space . (u - v) < e by A53, Def2;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by CLVECT_1:103 ;
hence  ||.((vseq . n) - tv).|| < e by A54; ::_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_1:def_15; ::_thesis: verum
end;