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

v + u in 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

for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_BoundedComplexSequences & u in the_set_of_BoundedComplexSequences holds
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;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

v + u in the_set_of_BoundedComplexSequences

proof

hence
the_set_of_BoundedComplexSequences is linearly-closed
by A1, CLVECT_1:def 7; :: thesis: verum
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;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