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 Nat holds 0 <= |.(seq_id (v + u)).| . n

proof

let n be 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 Nat holds |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n

proof

let n be Nat; :: thesis: |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n
A6: n in NAT by ORDINAL1:def 12;
A7: |.((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
.= |.(((seq_id v) . n) + ((seq_id u) . n)).| by VALUED_1:1, A6 ;
hence |.(seq_id (v + u)).| . n <= (|.(seq_id v).| + |.(seq_id u).|) . n by A7, COMPLEX1:56; :: thesis: verum

end;

seq_id u is absolutely_summable by A3, Def1;
then A8: |.(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 A8, 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; :: 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 A9: 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)).|;
A10: for n being Nat holds 0 <= |.(seq_id (a * v)).| . n

proof

let n be 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;

A11: for n being Nat holds |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n

proof

let n be Nat; :: thesis: |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n
|.(seq_id (a * v)).| . n = |.((seq_id (a * v)) . n).| by VALUED_1:18
.= |.((seq_id (a (#) (seq_id v))) . n).| by CSSPACE:3
.= |.(a (#) (seq_id v)).| . n by VALUED_1:18 ;
hence |.(seq_id (a * v)).| . n <= (|.a.| (#) |.(seq_id v).|) . n by COMSEQ_1:50; :: thesis: verum

end;

seq_id v is absolutely_summable by A9, 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 A10, A11, 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; :: thesis: verum

end;

hence the_set_of_l1ComplexSequences is linearly-closed by A1, CLVECT_1:def 7; :: thesis: verum