:: RSSPACE3 semantic presentation

begin

definition
func the_set_of_l1RealSequences  ->  Subset of Linear_Space_of_RealSequences means :Def1: :: RSSPACE3:def 1
 for x being set holds
( x in it iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) );
existence
 ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & 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_RealSequences & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in IT holds
x in the_set_of_RealSequences by A1;
then  IT is Subset of the_set_of_RealSequences by TARSKI:def_3;
hence  ex b1 being Subset of Linear_Space_of_RealSequences st
for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) by A1, RSSPACE:def_7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of Linear_Space_of_RealSequences st ( for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds
( x in b2 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) holds
b1 = b2
proof
let X1, X2 be Subset of Linear_Space_of_RealSequences; ::_thesis: ( ( for x being set holds
( x in X1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) ) & ( for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & 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_RealSequences & seq_id x is absolutely_summable ) ) and
A3: for x being set holds
( x in X2 iff ( x in the_set_of_RealSequences & 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_RealSequences & 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_RealSequences & 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_l1RealSequences RSSPACE3:def_1_:_
 for b1 being Subset of Linear_Space_of_RealSequences holds
( b1 = the_set_of_l1RealSequences iff for x being set holds
( x in b1 iff ( x in the_set_of_RealSequences & seq_id x is absolutely_summable ) ) );

theorem Th1: :: RSSPACE3:1
for c being Real
for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = abs ((lim seq) - c) )
proof
let c be Real; ::_thesis: for seq being Real_Sequence st seq is convergent holds
for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = abs ((lim seq) - c) )
reconsider cseq = NAT --> c as Real_Sequence ;
let seq be Real_Sequence; ::_thesis: ( seq is convergent implies for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = abs ((lim seq) - c) ) )
assume A1: seq is convergent ; ::_thesis: for rseq being Real_Sequence st ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) holds
( rseq is convergent & lim rseq = abs ((lim seq) - c) )
A2: seq - cseq is convergent by A1, SEQ_2:11;
then A3: abs (seq - cseq) is convergent ;
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ) implies ( rseq is convergent & lim rseq = abs ((lim seq) - c) ) )
assume A4: for i being Element of NAT holds rseq . i = abs ((seq . i) - c) ; ::_thesis: ( rseq is convergent & lim rseq = abs ((lim seq) - c) )
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_(abs_(seq_-_cseq))_._i
let i be Element of NAT ; ::_thesis: rseq . i = (abs (seq - cseq)) . i
thus rseq . i = abs ((seq . i) - c) by A4
.= abs ((seq . i) - (cseq . i)) by FUNCOP_1:7
.= abs ((seq . i) + (- (cseq . i)))
.= abs ((seq . i) + ((- cseq) . i)) by SEQ_1:10
.= abs ((seq + (- cseq)) . i) by SEQ_1:7
.= abs ((seq - cseq) . i) by SEQ_1:11
.= (abs (seq - cseq)) . i by SEQ_1:12 ; ::_thesis: verum
end;
then A5: for x being set st x in NAT holds
rseq . x = (abs (seq - cseq)) . x ;
lim (abs (seq - cseq)) = abs (lim (seq - cseq)) by A2, SEQ_4:14
.= abs ((lim seq) - (lim cseq)) by A1, SEQ_2:12
.= abs ((lim seq) - (cseq . 0)) by SEQ_4:26
.= abs ((lim seq) - c) by FUNCOP_1:7 ;
hence  ( rseq is convergent & lim rseq = abs ((lim seq) - c) ) by A5, A3, FUNCT_2:12; ::_thesis: verum
end;

registration
cluster the_set_of_l1RealSequences  ->  non empty ;
coherence
 not the_set_of_l1RealSequences is empty
proof
 seq_id Zeroseq is absolutely_summable
proof
reconsider rseq = seq_id Zeroseq as Real_Sequence ;
 for n being Element of NAT holds rseq . n = 0 by RSSPACE:def_6;
hence  seq_id Zeroseq is absolutely_summable by COMSEQ_3:3; ::_thesis: verum
end;
hence  not the_set_of_l1RealSequences is empty by Def1; ::_thesis: verum
end;
end;

registration
cluster the_set_of_l1RealSequences  ->  linearly-closed ;
coherence
 the_set_of_l1RealSequences is linearly-closed
proof
set W = the_set_of_l1RealSequences ;
A1: for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l1RealSequences & u in the_set_of_l1RealSequences holds
v + u in the_set_of_l1RealSequences
proof
let v, u be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_l1RealSequences & u in the_set_of_l1RealSequences implies v + u in the_set_of_l1RealSequences )
assume that
A2: v in the_set_of_l1RealSequences and
A3: u in the_set_of_l1RealSequences ; ::_thesis: v + u in the_set_of_l1RealSequences
 seq_id (v + u) is absolutely_summable
proof
set r = abs (seq_id (v + u));
set q = abs (seq_id u);
set p = abs (seq_id v);
A4: for n being Element of NAT holds 0 <= (abs (seq_id (v + u))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (abs (seq_id (v + u))) . n
 (abs (seq_id (v + u))) . n = abs ((seq_id (v + u)) . n) by SEQ_1:12;
hence  0 <= (abs (seq_id (v + u))) . n by COMPLEX1:46; ::_thesis: verum
end;
A5: for n being Element of NAT holds (abs (seq_id (v + u))) . n <= ((abs (seq_id v)) + (abs (seq_id u))) . n
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (v + u))) . n <= ((abs (seq_id v)) + (abs (seq_id u))) . n
A6: (abs ((seq_id v) . n)) + (abs ((seq_id u) . n)) = ((abs (seq_id v)) . n) + (abs ((seq_id u) . n)) by SEQ_1:12
.= ((abs (seq_id v)) . n) + ((abs (seq_id u)) . n) by SEQ_1:12
.= ((abs (seq_id v)) + (abs (seq_id u))) . n by SEQ_1:7 ;
(abs (seq_id (v + u))) . n = abs ((seq_id (v + u)) . n) by SEQ_1:12
.= abs ((seq_id ((seq_id v) + (seq_id u))) . n) by RSSPACE:2, RSSPACE:def_7
.= abs (((seq_id v) + (seq_id u)) . n) by RSSPACE:1
.= abs (((seq_id v) . n) + ((seq_id u) . n)) by SEQ_1:7 ;
hence  (abs (seq_id (v + u))) . n <= ((abs (seq_id v)) + (abs (seq_id u))) . n by A6, COMPLEX1:56; ::_thesis: verum
end;
 seq_id u is absolutely_summable by A3, Def1;
then A7: abs (seq_id u) is summable by SERIES_1:def_4;
 seq_id v is absolutely_summable by A2, Def1;
then  abs (seq_id v) is summable by SERIES_1:def_4;
then  (abs (seq_id v)) + (abs (seq_id u)) is summable by A7, SERIES_1:7;
then  abs (seq_id (v + u)) is summable by A4, A5, SERIES_1:20;
hence  seq_id (v + u) is absolutely_summable by SERIES_1:def_4; ::_thesis: verum
end;
hence  v + u in the_set_of_l1RealSequences by Def1, RSSPACE:def_7; ::_thesis: verum
end;
 for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l1RealSequences holds
a * v in the_set_of_l1RealSequences
proof
let a be Real; ::_thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l1RealSequences holds
a * v in the_set_of_l1RealSequences
let v be VECTOR of Linear_Space_of_RealSequences; ::_thesis: ( v in the_set_of_l1RealSequences implies a * v in the_set_of_l1RealSequences )
assume A8: v in the_set_of_l1RealSequences ; ::_thesis: a * v in the_set_of_l1RealSequences
 seq_id (a * v) is absolutely_summable
proof
set r1 = (abs a) (#) (abs (seq_id v));
set q1 = abs (seq_id (a * v));
A9: for n being Element of NAT holds 0 <= (abs (seq_id (a * v))) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (abs (seq_id (a * v))) . n
 (abs (seq_id (a * v))) . n = abs ((seq_id (a * v)) . n) by SEQ_1:12;
hence  0 <= (abs (seq_id (a * v))) . n by COMPLEX1:46; ::_thesis: verum
end;
A10: for n being Element of NAT holds (abs (seq_id (a * v))) . n <= ((abs a) (#) (abs (seq_id v))) . n
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (a * v))) . n <= ((abs a) (#) (abs (seq_id v))) . n
(abs (seq_id (a * v))) . n = abs ((seq_id (a * v)) . n) by SEQ_1:12
.= abs ((seq_id (a (#) (seq_id v))) . n) by RSSPACE:3, RSSPACE:def_7
.= abs ((a (#) (seq_id v)) . n) by RSSPACE:1
.= (abs (a (#) (seq_id v))) . n by SEQ_1:12 ;
hence  (abs (seq_id (a * v))) . n <= ((abs a) (#) (abs (seq_id v))) . n by SEQ_1:56; ::_thesis: verum
end;
 seq_id v is absolutely_summable by A8, Def1;
then  abs (seq_id v) is summable by SERIES_1:def_4;
then  (abs a) (#) (abs (seq_id v)) is summable by SERIES_1:10;
then  abs (seq_id (a * v)) is summable by A9, A10, SERIES_1:20;
hence  seq_id (a * v) is absolutely_summable by SERIES_1:def_4; ::_thesis: verum
end;
hence  a * v in the_set_of_l1RealSequences by Def1, RSSPACE:def_7; ::_thesis: verum
end;
hence  the_set_of_l1RealSequences is linearly-closed by A1, RLSUB_1:def_1; ::_thesis: verum
end;
end;

Lm1:  RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Subspace of Linear_Space_of_RealSequences
by RSSPACE:11;

registration
cluster RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) ->  right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;
coherence
 ( RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is Abelian & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is add-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_zeroed & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is right_complementable & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is vector-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-distributive & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-associative & RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is scalar-unital ) by RSSPACE:11;
end;

Lm2:  RLSStruct(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)) #) is RealLinearSpace
;

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

:: deftheorem Def2 defines l_norm RSSPACE3:def_2_:_
 for b1 being Function of the_set_of_l1RealSequences,REAL holds
( b1 = l_norm iff for x being set st x in the_set_of_l1RealSequences holds
b1 . x = Sum (abs (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 [:REAL,X:],X;
let N be Function of X,REAL;
cluster NORMSTR(# X,Z,A,M,N #) ->  non empty ;
coherence
 not NORMSTR(# X,Z,A,M,N #) is empty ;
end;

theorem :: RSSPACE3:2
for l being NORMSTR st RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace by RSSPACE:15;

theorem Th3: :: RSSPACE3:3
for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds
( rseq is absolutely_summable & Sum (abs rseq) = 0 )
proof
let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies ( rseq is absolutely_summable & Sum (abs rseq) = 0 ) )
assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: ( rseq is absolutely_summable & Sum (abs rseq) = 0 )
A2: for n being Element of NAT holds (abs rseq) . n = 0
proof
let n be Element of NAT ; ::_thesis: (abs rseq) . n = 0
 ( rseq . n = 0 & (abs rseq) . n = abs (rseq . n) ) by A1, SEQ_1:12;
hence  (abs rseq) . n = 0 by ABSVALUE:2; ::_thesis: verum
end;
A3: for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0
proof
defpred S1[ Element of NAT ] means (abs rseq) . $1 = (Partial_Sums (abs rseq)) . $1;
let m be Element of NAT ; ::_thesis: (Partial_Sums (abs rseq)) . 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: (abs rseq) . k = (Partial_Sums (abs rseq)) . k ; ::_thesis: S1[k + 1]
thus (abs rseq) . (k + 1) = 0 + ((abs rseq) . (k + 1))
.= ((abs rseq) . k) + ((abs rseq) . (k + 1)) by A2
.= (Partial_Sums (abs rseq)) . (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 (abs rseq)) . m = (abs rseq) . 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 (abs rseq)) . 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 (abs rseq)) . 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 (abs rseq)) . m) - 0) < p
take  0 ; ::_thesis: for m being Element of NAT st 0 <= m holds
abs (((Partial_Sums (abs rseq)) . m) - 0) < p
let m be Element of NAT ; ::_thesis: ( 0 <= m implies abs (((Partial_Sums (abs rseq)) . m) - 0) < p )
assume  0 <= m ; ::_thesis: abs (((Partial_Sums (abs rseq)) . m) - 0) < p
abs (((Partial_Sums (abs rseq)) . m) - 0) = abs (0 - 0) by A3
.= 0 by ABSVALUE:def_1 ;
hence  abs (((Partial_Sums (abs rseq)) . m) - 0) < p by A8; ::_thesis: verum
end;
then A9: Partial_Sums (abs rseq) is convergent by SEQ_2:def_6;
then A10: abs rseq is summable by SERIES_1:def_2;
 lim (Partial_Sums (abs rseq)) = 0 by A7, A9, SEQ_2:def_7;
hence  ( rseq is absolutely_summable & Sum (abs rseq) = 0 ) by A10, SERIES_1:def_3, SERIES_1:def_4; ::_thesis: verum
end;

theorem Th4: :: RSSPACE3:4
for rseq being Real_Sequence st rseq is absolutely_summable & Sum (abs rseq) = 0 holds
for n being Element of NAT holds rseq . n = 0
proof
let rseq be Real_Sequence; ::_thesis: ( rseq is absolutely_summable & Sum (abs rseq) = 0 implies for n being Element of NAT holds rseq . n = 0 )
assume that
A1: rseq is absolutely_summable and
A2: Sum (abs rseq) = 0 ; ::_thesis: for n being Element of NAT holds rseq . n = 0
reconsider arseq = abs rseq as Real_Sequence ;
A3: for n being Element of NAT holds 0 <= (abs rseq) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (abs rseq) . n
 0 <= abs (rseq . n) by COMPLEX1:46;
hence  0 <= (abs rseq) . n by SEQ_1:12; ::_thesis: verum
end;
A4: arseq is summable by A1, SERIES_1:def_4;
 for n being Element of NAT holds rseq . n = 0
proof
let n be Element of NAT ; ::_thesis: rseq . n = 0
 (abs rseq) . n = 0 by A2, A4, A3, RSSPACE:17;
then  abs (rseq . n) = 0 by SEQ_1:12;
hence  rseq . n = 0 by ABSVALUE:2; ::_thesis: verum
end;
hence  for n being Element of NAT holds rseq . n = 0 ; ::_thesis: verum
end;

theorem Th5: :: RSSPACE3:5
NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #) is RealLinearSpace by Lm2, RSSPACE:15;

definition
func l1_Space  ->  non empty NORMSTR  equals :: RSSPACE3:def 3
 NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #);
coherence
 NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #) is non empty NORMSTR ;
end;

:: deftheorem  defines l1_Space RSSPACE3:def_3_:_
 l1_Space = NORMSTR(# the_set_of_l1RealSequences,(Zero_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Add_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),(Mult_ (the_set_of_l1RealSequences,Linear_Space_of_RealSequences)),l_norm #);

begin

theorem Th6: :: RSSPACE3:6
( the carrier of l1_Space = the_set_of_l1RealSequences & ( for x being set holds
( x is VECTOR of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) ) & 0. l1_Space = Zeroseq & ( for u being VECTOR of l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) ) )
proof
set l1 = l1_Space ;
A1: for x being set holds
( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) )
proof
let x be set ; ::_thesis: ( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) )
 ( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def_1;
hence  ( x is Element of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) by Def1; ::_thesis: verum
end;
A2: for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v)
proof
let u, v be VECTOR of l1_Space; ::_thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l1RealSequences ;
 dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then  dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) = [:the_set_of_l1RealSequences,the_set_of_l1RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A3: [u,v] in dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) by ZFMISC_1:87;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l1RealSequences) . [u,v] by RSSPACE:def_8
.= u1 + v1 by A3, FUNCT_1:47 ;
hence  u + v = (seq_id u) + (seq_id v) by RSSPACE:2, RSSPACE:def_7; ::_thesis: verum
end;
A4: for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u)
proof
let r be Real; ::_thesis: for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of l1_Space; ::_thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l1RealSequences ;
 dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def_1;
then  dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) = [:REAL,the_set_of_l1RealSequences:] by RELAT_1:62, ZFMISC_1:96;
then A5: [r,u] in dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) by ZFMISC_1:87;
r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l1RealSequences:]) . [r,u] by RSSPACE:def_9
.= r * u1 by A5, FUNCT_1:47 ;
hence  r * u = r (#) (seq_id u) by RSSPACE:3, RSSPACE:def_7; ::_thesis: verum
end;
A6: for u being VECTOR of l1_Space holds u = seq_id u
proof
let u be VECTOR of l1_Space; ::_thesis: u = seq_id u
 u is VECTOR of Linear_Space_of_RealSequences by Lm1, RLSUB_1:10;
hence  u = seq_id u by RSSPACE:def_2, RSSPACE:def_7; ::_thesis: verum
end;
A7: for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
proof
let u be VECTOR of l1_Space; ::_thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by Th5, RLVECT_1:16
.= (- 1) (#) (seq_id u) by A4
.= - (seq_id u) by SEQ_1:17 ;
hence  ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A6; ::_thesis: verum
end;
A8: for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v)
proof
let u, v be VECTOR of 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
.= (seq_id u) - (seq_id v) by SEQ_1:11 ; ::_thesis: verum
end;
A9: for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) by Def2;
0. l1_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def_10
.= Zeroseq by RSSPACE:def_7 ;
hence  ( the carrier of l1_Space = the_set_of_l1RealSequences & ( for x being set holds
( x is VECTOR of l1_Space iff ( x is Real_Sequence & seq_id x is absolutely_summable ) ) ) & 0. l1_Space = Zeroseq & ( for u being VECTOR of l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l1_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of l1_Space holds ||.v.|| = Sum (abs (seq_id v)) ) ) by A1, A6, A2, A4, A7, A8, A9; ::_thesis: verum
end;

theorem Th7: :: RSSPACE3:7
for x, y being Point of l1_Space
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
proof
let x, y be Point of l1_Space; ::_thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
let a be Real; ::_thesis: ( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
A1: for n being Element of NAT holds 0 <= (abs (seq_id x)) . n
proof
let n be Element of NAT ; ::_thesis: 0 <= (abs (seq_id x)) . n
 0 <= abs ((seq_id x) . n) by COMPLEX1:46;
hence  0 <= (abs (seq_id x)) . n by SEQ_1:12; ::_thesis: verum
end;
A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(abs_(seq_id_(x_+_y)))_._n
let n be Element of NAT ; ::_thesis: 0 <= (abs (seq_id (x + y))) . n
 (abs (seq_id (x + y))) . n = abs ((seq_id (x + y)) . n) by SEQ_1:12;
hence  0 <= (abs (seq_id (x + y))) . n by COMPLEX1:46; ::_thesis: verum
end;
A3: for n being Element of NAT holds (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n))
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n))
(abs (seq_id (x + y))) . n = (abs (seq_id ((seq_id x) + (seq_id y)))) . n by Th6
.= (abs ((seq_id x) + (seq_id y))) . n by RSSPACE:1
.= abs (((seq_id x) + (seq_id y)) . n) by SEQ_1:12
.= abs (((seq_id x) . n) + ((seq_id y) . n)) by SEQ_1:7 ;
hence  (abs (seq_id (x + y))) . n = abs (((seq_id x) . n) + ((seq_id y) . n)) ; ::_thesis: verum
end;
A4: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n)
 abs (((seq_id x) . n) + ((seq_id y) . n)) <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by COMPLEX1:56;
then  (abs (seq_id (x + y))) . n <= (abs ((seq_id x) . n)) + (abs ((seq_id y) . n)) by A3;
then  (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + (abs ((seq_id y) . n)) by SEQ_1:12;
hence  (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) by SEQ_1:12; ::_thesis: verum
end;
A5: for n being Element of NAT holds (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n
proof
let n be Element of NAT ; ::_thesis: (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n
 ((abs (seq_id x)) . n) + ((abs (seq_id y)) . n) = ((abs (seq_id x)) + (abs (seq_id y))) . n by SEQ_1:7;
hence  (abs (seq_id (x + y))) . n <= ((abs (seq_id x)) + (abs (seq_id y))) . n by A4; ::_thesis: verum
end;
 seq_id y is absolutely_summable by Def1;
then A6: abs (seq_id y) is summable by SERIES_1:def_4;
 seq_id x is absolutely_summable by Def1;
then  abs (seq_id x) is summable by SERIES_1:def_4;
then  (abs (seq_id x)) + (abs (seq_id y)) is summable by A6, SERIES_1:7;
then A7: Sum (abs (seq_id (x + y))) <= Sum ((abs (seq_id x)) + (abs (seq_id y))) by A5, A2, SERIES_1:20;
A8: now__::_thesis:_(_x_=_0._l1_Space_implies_||.x.||_=_0_)
assume  x = 0. l1_Space ; ::_thesis: ||.x.|| = 0
then A9: for n being Element of NAT holds (seq_id x) . n = 0 by Th6, RSSPACE:def_6;
thus ||.x.|| = the normF of l1_Space . x
.= Sum (abs (seq_id x)) by Def2
.= 0 by A9, Th3 ; ::_thesis: verum
end;
A10: Sum (abs (seq_id (x + y))) = ||.(x + y).|| by Th6;
A11: now__::_thesis:_(_||.x.||_=_0_implies_x_=_0._l1_Space_)
A12: x in the_set_of_RealSequences by Def1;
assume A13: ||.x.|| = 0 ; ::_thesis: x = 0. l1_Space
 ( ||.x.|| = Sum (abs (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. l1_Space by A12, Th6, RSSPACE:def_6; ::_thesis: verum
end;
A14: ( ||.x.|| = Sum (abs (seq_id x)) & ||.y.|| = Sum (abs (seq_id y)) ) by Th6;
A15: for n being Element of NAT holds (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)
proof
let n be Element of NAT ; ::_thesis: (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n)
(abs (a (#) (seq_id x))) . n = abs ((a (#) (seq_id x)) . n) by SEQ_1:12
.= abs (a * ((seq_id x) . n)) by SEQ_1:9
.= (abs a) * (abs ((seq_id x) . n)) by COMPLEX1:65
.= (abs a) * ((abs (seq_id x)) . n) by SEQ_1:12 ;
hence  (abs (a (#) (seq_id x))) . n = (abs a) * ((abs (seq_id x)) . n) ; ::_thesis: verum
end;
 seq_id x is absolutely_summable by Def1;
then A16: abs (seq_id x) is summable by SERIES_1:def_4;
 seq_id x is absolutely_summable by Def1;
then A17: abs (seq_id x) is summable by SERIES_1:def_4;
||.(a * x).|| = Sum (abs (seq_id (a * x))) by Th6
.= Sum (abs (seq_id (a (#) (seq_id x)))) by Th6
.= Sum (abs (a (#) (seq_id x))) by RSSPACE:1
.= Sum ((abs a) (#) (abs (seq_id x))) by A15, SEQ_1:9
.= (abs a) * (Sum (abs (seq_id x))) by A16, SERIES_1:10
.= (abs a) * ||.x.|| by Th6 ;
hence  ( ( ||.x.|| = 0 implies x = 0. l1_Space ) & ( x = 0. l1_Space implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| ) by A11, A8, A1, A17, A14, A10, A6, A7, SERIES_1:7, SERIES_1:18; ::_thesis: verum
end;

registration
cluster l1_Space  ->  non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;
coherence
 ( l1_Space is reflexive & l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )
proof
thus  ||.(0. l1_Space).|| = 0 by Th7; :: according to NORMSP_0:def_6 ::_thesis: ( l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )
thus  ( l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable ) by Lm2, Th7, NORMSP_0:def_5, NORMSP_1:def_1, RSSPACE:15; ::_thesis: verum
end;
end;

Lm3:  for c being Real
for seq, 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 = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
proof
let c be Real; ::_thesis: for seq, 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 = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
let seq, 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 = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((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 = (abs ((seq . i) - c)) + (seq1 . i) ) holds
( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
reconsider cseq = NAT --> c as Real_Sequence ;
A3: seq - cseq is convergent by A1, SEQ_2:11;
then A4: abs (seq - cseq) is convergent ;
let rseq be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ) implies ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) ) )
assume A5: for i being Element of NAT holds rseq . i = (abs ((seq . i) - c)) + (seq1 . i) ; ::_thesis: ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) )
now__::_thesis:_for_i_being_Element_of_NAT_holds_rseq_._i_=_((abs_(seq_-_cseq))_+_seq1)_._i
let i be Element of NAT ; ::_thesis: rseq . i = ((abs (seq - cseq)) + seq1) . i
thus rseq . i = (abs ((seq . i) - c)) + (seq1 . i) by A5
.= (abs ((seq . i) - (cseq . i))) + (seq1 . i) by FUNCOP_1:7
.= (abs ((seq . i) + (- (cseq . i)))) + (seq1 . i)
.= (abs ((seq . i) + ((- cseq) . i))) + (seq1 . i) by SEQ_1:10
.= (abs ((seq + (- cseq)) . i)) + (seq1 . i) by SEQ_1:7
.= (abs ((seq - cseq) . i)) + (seq1 . i) by SEQ_1:11
.= ((abs (seq - cseq)) . i) + (seq1 . i) by SEQ_1:12
.= ((abs (seq - cseq)) + seq1) . i by SEQ_1:7 ; ::_thesis: verum
end;
then A6: rseq = (abs (seq - cseq)) + seq1 by FUNCT_2:63;
lim (abs (seq - cseq)) = abs (lim (seq - cseq)) by A3, SEQ_4:14
.= abs ((lim seq) - (lim cseq)) by A1, SEQ_2:12
.= abs ((lim seq) - (cseq . 0)) by SEQ_4:26
.= abs ((lim seq) - c) by FUNCOP_1:7 ;
hence  ( rseq is convergent & lim rseq = (abs ((lim seq) - c)) + (lim seq1) ) by A2, A6, A4, SEQ_2:5, SEQ_2:6; ::_thesis: verum
end;

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

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

definition
let NRM be non empty NORMSTR ;
let seqt be sequence of NRM;
attrseqt is CCauchy  means :Def5: :: RSSPACE3: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 RSSPACE3:def_5_:_
 for NRM being non empty NORMSTR
for seqt being sequence of NRM 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 NRM be non empty NORMSTR ;
let seqt be sequence of NRM;
synonym  Cauchy_sequence_by_Norm seqt for  CCauchy ;
end;


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