set W = the_set_of_l2RealSequences ;
A1: 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 A2: ( v in the_set_of_l2RealSequences & 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

A3: (seq_id v) (#) (seq_id v) is summable by A2, Def11;
A4: (seq_id u) (#) (seq_id u) is summable by A2, Def11;
set p = (seq_id v) (#) (seq_id v);
set q = (seq_id u) (#) (seq_id u);
set r = (seq_id (v + u)) (#) (seq_id (v + u));
A5: 2 (#) ((seq_id v) (#) (seq_id v)) is summable by A3, SERIES_1:13;
2 (#) ((seq_id u) (#) (seq_id u)) is summable by A4, SERIES_1:13;
then A6: (2 (#) ((seq_id v) (#) (seq_id v))) + (2 (#) ((seq_id u) (#) (seq_id u))) is summable by A5, SERIES_1:10;
A7: 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:12;
hence 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n by XREAL_1:65; :: thesis: verum

end;

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

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
set s = seq_id v;
set t = seq_id u;
reconsider sn = (seq_id v) . n, tn = (seq_id u) . n as Real ;
A8: seq_id (v + u) = seq_id ((seq_id v) + (seq_id u)) by Def4
.= (seq_id v) + (seq_id u) by Th3 ;
A9: ((seq_id (v + u)) (#) (seq_id (v + u))) . n = ((seq_id (v + u)) . n) * ((seq_id (v + u)) . n) by SEQ_1:12
.= (((seq_id v) . n) + ((seq_id u) . n)) * (((seq_id v) + (seq_id u)) . n) by A8, SEQ_1:11
.= (((seq_id v) . n) + ((seq_id u) . n)) ^2 by SEQ_1:11
.= ((sn ^2 ) + ((2 * sn) * tn)) + (tn ^2 ) ;
A10: ((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:11
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + ((2 (#) ((seq_id u) (#) (seq_id u))) . n) by SEQ_1:13
.= (2 * (((seq_id v) (#) (seq_id v)) . n)) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:13
.= (2 * (((seq_id v) . n) * ((seq_id v) . n))) + (2 * (((seq_id u) (#) (seq_id u)) . n)) by SEQ_1:12
.= (2 * (sn ^2 )) + (2 * (tn ^2 )) by SEQ_1:12 ;
0 <= (sn - tn) ^2 by XREAL_1:65;
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 A9, A10, XREAL_1:9;
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;

hence (seq_id (v + u)) (#) (seq_id (v + u)) is summable by A6, A7, SERIES_1:24; :: thesis: verum

end;

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

end;

A11: not the_set_of_l2RealSequences is empty

proof

(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:12
.= ((seq_id Zeroseq ) . n) * 0 by Def6
.= 0 ; :: thesis: verum

end;

then rseq is absolutely_summable by COMSEQ_3:3;
hence (seq_id Zeroseq ) (#) (seq_id Zeroseq ) is summable by SERIES_1:40; :: thesis: verum

end;

hence not the_set_of_l2RealSequences is empty by Def11; :: thesis: verum

end;

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 A12: v in the_set_of_l2RealSequences ; :: thesis: a * v in the_set_of_l2RealSequences
(seq_id (a * v)) (#) (seq_id (a * v)) is summable

proof

A13: (seq_id v) (#) (seq_id v) is summable by A12, 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:27
.= a (#) (a (#) ((seq_id v) (#) (seq_id v))) by SEQ_1:26
.= (a * a) (#) ((seq_id v) (#) (seq_id v)) by SEQ_1:31 ;
hence (seq_id (a * v)) (#) (seq_id (a * v)) is summable by A13, SERIES_1:13; :: thesis: verum

end;

hence a * v in the_set_of_l2RealSequences by Def11; :: thesis: verum

end;

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