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

proof

let a be Real; :: thesis: for v being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l2RealSequences holds
a * v in the_set_of_l2RealSequences
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis: ( v in the_set_of_l2RealSequences implies a * v in the_set_of_l2RealSequences )
assume v in the_set_of_l2RealSequences ; :: thesis: a * v in the_set_of_l2RealSequences
then A2: (seq_id v) (#) (seq_id v) is summable by Def11;
seq_id (a * v) = seq_id (a (#) (seq_id v)) by Th5
.= a (#) (seq_id v) by Th3 ;
then (seq_id (a * v)) (#) (seq_id (a * v)) = a (#) ((a (#) (seq_id v)) (#) (seq_id v)) by SEQ_1:19
.= a (#) (a (#) ((seq_id v) (#) (seq_id v))) by SEQ_1:18
.= (a * a) (#) ((seq_id v) (#) (seq_id v)) by SEQ_1:23 ;
then (seq_id (a * v)) (#) (seq_id (a * v)) is summable by A2, SERIES_1:10;
hence a * v in the_set_of_l2RealSequences by Def11; :: thesis: verum

end;

A3: for v, u being VECTOR of Linear_Space_of_RealSequences st v in the_set_of_l2RealSequences & u in the_set_of_l2RealSequences holds
v + u in the_set_of_l2RealSequences

proof

let v, u be VECTOR of Linear_Space_of_RealSequences; :: thesis: ( v in the_set_of_l2RealSequences & u in the_set_of_l2RealSequences implies v + u in the_set_of_l2RealSequences )
assume that
A4: v in the_set_of_l2RealSequences and
A5: u in the_set_of_l2RealSequences ; :: thesis: v + u in the_set_of_l2RealSequences
(seq_id (v + u)) (#) (seq_id (v + u)) is summable

proof

set r = (seq_id (v + u)) (#) (seq_id (v + u));
set q = (seq_id u) (#) (seq_id u);
set p = (seq_id v) (#) (seq_id v);
A6: for n being Element of NAT holds 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n

proof

let n be Element of NAT ; :: thesis: 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n
((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((seq_id (v + u)) . n) * ((seq_id (v + u)) . n) by SEQ_1:8;
hence 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n by XREAL_1:63; :: thesis: verum

end;

A7: for n being Element of NAT holds ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n

proof

set s = seq_id v;
set t = seq_id u;
let n be Element of NAT ; :: thesis: ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n
reconsider sn = (seq_id v) . n, tn = (seq_id u) . n as Real ;
A8: ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n = ((2 (#) ((seq_id v) (#) (seq_id v))) . n) + ((2 (#) ((seq_id u) (#) (seq_id u))) . n) by SEQ_1:7
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + ((2 (#) ((seq_id u) (#) (seq_id u))) . n) by SEQ_1:9
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:9
.= (2 * (((seq_id v) . n) * ((seq_id v) . n))) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:8
.= (2 * (sn ^2)) + (2 * (tn ^2)) by SEQ_1:8 ;
A9: 0 <= (sn - tn) ^2 by XREAL_1:63;
A10: seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by Def4
.= (seq_id v) + (seq_id u) by Th3 ;
((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((seq_id (v + u)) . n) * ((seq_id (v + u)) . n) by SEQ_1:8
.= (((seq_id v) . n) + ((seq_id u) . n)) * (((seq_id v) + (seq_id u)) . n) by A10, SEQ_1:7
.= (((seq_id v) . n) + ((seq_id u) . n)) ^2 by SEQ_1:7
.= ((sn ^2) + ((2 * sn) * tn)) + (tn ^2) ;
then 0 + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) <= ((((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n) - (((seq_id (v + u)) (#) (seq_id (v + u))) . n)) + (((seq_id (v + u)) (#) (seq_id (v + u))) . n) by A8, A9, XREAL_1:7;
hence ((seq_id (v + u)) (#) (seq_id (v + u))) . n <= ((2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u)))) . n ; :: thesis: verum

end;

(seq_id u) (#) (seq_id u) is summable by A5, Def11;
then A11: 2 (#) ((seq_id u) (#) (seq_id u)) is summable by SERIES_1:10;
(seq_id v) (#) (seq_id v) is summable by A4, Def11;
then 2 (#) ((seq_id v) (#) (seq_id v)) is summable by SERIES_1:10;
then (2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u))) is summable by A11, SERIES_1:7;
hence (seq_id (v + u)) (#) (seq_id (v + u)) is summable by A6, A7, SERIES_1:20; :: thesis: verum

end;

hence v + u in the_set_of_l2RealSequences by Def11; :: thesis: verum

end;

(seq_id Zeroseq) (#) (seq_id Zeroseq) is summable

proof

reconsider rseq = (seq_id Zeroseq) (#) (seq_id Zeroseq) as Real_Sequence ;

now

let n be Element of NAT ; :: thesis: rseq . n = 0
thus rseq . n = ((seq_id Zeroseq) . n) * ((seq_id Zeroseq) . n) by SEQ_1:8
.= ((seq_id Zeroseq) . n) * 0 by Def6
.= 0 ; :: thesis: verum

end;

hence (seq_id Zeroseq) (#) (seq_id Zeroseq) is summable by COMSEQ_3:3, SERIES_1:35; :: thesis: verum

end;

hence ( the_set_of_l2RealSequences is linearly-closed & not the_set_of_l2RealSequences is empty ) by A3, A1, Def11, RLSUB_1:def 1; :: thesis: verum