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

proof

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

proof

let n be Nat; :: thesis: (abs (seq_id (v + u))) . n <= ((abs (seq_id v)) + (abs (seq_id u))) . n
A6: |.((seq_id v) . n).| + |.((seq_id u) . n).| = ((abs (seq_id v)) . n) + |.((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 = |.((seq_id (v + u)) . n).| by SEQ_1:12
.= |.((seq_id ((seq_id v) + (seq_id u))) . n).| by RSSPACE:2
.= |.(((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; :: 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 = |.a.| (#) (abs (seq_id v));
set q1 = abs (seq_id (a * v));
A9: for n being Nat holds 0 <= (abs (seq_id (a * v))) . n

proof

let n be Nat; :: thesis: 0 <= (abs (seq_id (a * v))) . n
(abs (seq_id (a * v))) . n = |.((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 Nat holds (abs (seq_id (a * v))) . n <= (|.a.| (#) (abs (seq_id v))) . n

proof

let n be Nat; :: thesis: (abs (seq_id (a * v))) . n <= (|.a.| (#) (abs (seq_id v))) . n
(abs (seq_id (a * v))) . n = |.((seq_id (a * v)) . n).| by SEQ_1:12
.= |.((seq_id (a (#) (seq_id v))) . n).| by RSSPACE:3
.= (abs (a (#) (seq_id v))) . n by SEQ_1:12 ;
hence (abs (seq_id (a * v))) . n <= (|.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 |.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; :: thesis: verum

end;

hence the_set_of_l1RealSequences is linearly-closed by A1, RLSUB_1:def 1; :: thesis: verum