set W = the_set_of_l2RealSequences ;

hereby :: according to RLSUB_1:def 1 :: thesis: ( ( for b₁ being object
for b₂ being Element of the carrier of Linear_Space_of_RealSequences holds
( not b₂ in the_set_of_l2RealSequences or b₁ * b₂ in the_set_of_l2RealSequences ) ) & not the_set_of_l2RealSequences is empty )

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 Nat holds 0 <= ((seq_id (v + u)) (#) (seq_id (v + u))) . n

proof

let n be 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 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 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;
reconsider vu = v + u as Element of Funcs (NAT,REAL) ;
n in NAT by ORDINAL1:def 12;
then vu . n = ((seq_id v) . n) + ((seq_id u) . n) by FUNCSDOM:1;
then ((seq_id (v + u)) (#) (seq_id (v + u))) . n = (((seq_id v) . n) + ((seq_id u) . n)) ^2 by SEQ_1:8
.= ((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, Def8;
then A10: 2 (#) ((seq_id u) (#) (seq_id u)) is summable by SERIES_1:10;
(seq_id v) (#) (seq_id v) is summable by A4, Def8;
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 A10, 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 Def8; :: thesis: verum

end;

hereby :: thesis: not the_set_of_l2RealSequences is empty

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 Def8;
a * v = 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 Def8; :: thesis: verum

end;

(seq_id Zeroseq) (#) (seq_id Zeroseq) is absolutely_summable

proof

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

now :: thesis: for n being Nat holds rseq . n = 0

let n be 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 FUNCOP_1:7, ORDINAL1:def 12
.= 0 ; :: thesis: verum

end;

hence (seq_id Zeroseq) (#) (seq_id Zeroseq) is absolutely_summable by COMSEQ_3:3; :: thesis: verum

end;

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