set W = the_set_of_BoundedComplexSequences ;
A1: for c being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds
c * v in the_set_of_BoundedComplexSequences

proof

let c be Complex; :: thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences holds
c * v in the_set_of_BoundedComplexSequences
let v be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: ( v in the_set_of_BoundedComplexSequences implies c * v in the_set_of_BoundedComplexSequences )
assume v in the_set_of_BoundedComplexSequences ; :: thesis: c * v in the_set_of_BoundedComplexSequences
then A2: seq_id v is bounded by Def1;
seq_id (c * v) = seq_id (c (#) (seq_id v)) by CSSPACE:3
.= c (#) (seq_id v) ;
then seq_id (c * v) is bounded by A2, Lm4;
hence c * v in the_set_of_BoundedComplexSequences by Def1; :: thesis: verum

end;

for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences holds
v + u in the_set_of_BoundedComplexSequences

proof

let v, u be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences implies v + u in the_set_of_BoundedComplexSequences )
assume ( v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences ) ; :: thesis: v + u in the_set_of_BoundedComplexSequences
then A3: ( seq_id v is bounded & seq_id u is bounded ) by Def1;
seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by CSSPACE:2
.= (seq_id v) + (seq_id u) ;
then seq_id (v + u) is bounded by A3, Lm3;
hence v + u in the_set_of_BoundedComplexSequences by Def1; :: thesis: verum

end;

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