set W = the_set_of_BoundedRealSequences ;
A1: for a being Real
for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds
a * v in the_set_of_BoundedRealSequences

proof

let a be Real; :: thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences holds
a * v in the_set_of_BoundedRealSequences
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis: ( v in the_set_of_BoundedRealSequences implies a * v in the_set_of_BoundedRealSequences )
assume v in the_set_of_BoundedRealSequences ; :: thesis: a * v in the_set_of_BoundedRealSequences
then A2: seq_id v is bounded by Def1;
seq_id (a * v) = a (#) (seq_id v) by RSSPACE:3;
then seq_id (a * v) is bounded by A2, SEQM_3:37;
hence a * v in the_set_of_BoundedRealSequences by Def1; :: thesis: verum

end;

for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences holds
v + u in the_set_of_BoundedRealSequences

proof

let v, u be VECTOR of Linear_Space_of_RealSequences; :: thesis: ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences implies v + u in the_set_of_BoundedRealSequences )
assume ( v in the_set_of_BoundedRealSequences & u in the_set_of_BoundedRealSequences ) ; :: thesis: v + u in the_set_of_BoundedRealSequences
then A3: ( seq_id v is bounded & seq_id u is bounded ) by Def1;
seq_id (v + u) = (seq_id v) + (seq_id u) by RSSPACE:2;
hence v + u in the_set_of_BoundedRealSequences by A3, Def1; :: thesis: verum

end;

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