set W = the_set_of_l2ComplexSequences ;
A1: for v, u being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences & u in the_set_of_l2ComplexSequences holds
v + u in the_set_of_l2ComplexSequences

proof

let v, u be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: ( v in the_set_of_l2ComplexSequences & u in the_set_of_l2ComplexSequences implies v + u in the_set_of_l2ComplexSequences )
assume that
A2: v in the_set_of_l2ComplexSequences and
A3: u in the_set_of_l2ComplexSequences ; :: thesis: v + u in the_set_of_l2ComplexSequences
|.(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).|;
A4: 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;

A5: 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 t = |.(seq_id u).|;
set s = |.(seq_id v).|;
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 ;
A6: (|.(seq_id (v + u)).| (#) |.(seq_id (v + u)).|) . n = (|.(seq_id (v + u)).| . n) ^2 by SEQ_1:8;
((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 ;
then A7: (((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n) - (((sn ^2) + ((2 * sn) * tn)) + (tn ^2)) = (sn - tn) ^2 ;
A8: 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)).| . n = |.((seq_id (v + u)) . n).| by VALUED_1:18
.= |.(((seq_id v) . n) + ((seq_id u) . n)).| by A8, VALUED_1:1 ;
then |.(seq_id (v + u)).| . n <= |.((seq_id v) . n).| + |.((seq_id u) . n).| by COMPLEX1:56;
then |.(seq_id (v + u)).| . n <= (|.(seq_id v).| . n) + |.((seq_id u) . n).| by VALUED_1:18;
then A9: |.(seq_id (v + u)).| . n <= (|.(seq_id v).| . n) + (|.(seq_id u).| . n) by VALUED_1:18;
0 <= (sn - tn) ^2 by XREAL_1:63;
then A10: 0 + (((sn ^2) + ((2 * sn) * tn)) + (tn ^2)) <= ((2 (#) (|.(seq_id v).| (#) |.(seq_id v).|)) + (2 (#) (|.(seq_id u).| (#) |.(seq_id u).|))) . n by A7, XREAL_1:19;
0 <= |.((seq_id (v + u)) . n).| by COMPLEX1:46;
then 0 <= |.(seq_id (v + u)).| . n by VALUED_1:18;
then (|.(seq_id (v + u)).| . n) ^2 <= ((|.(seq_id v).| . n) + (|.(seq_id u).| . n)) ^2 by A9, SQUARE_1:15;
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 by A6, A10, XXREAL_0:2; :: thesis: verum

end;

|.(seq_id u).| (#) |.(seq_id u).| is summable by A3, 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 A2, 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 A4, A5, SERIES_1:20; :: thesis: verum

end;

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

end;

for z being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences holds
z * v in the_set_of_l2ComplexSequences

proof

let z be Complex; :: thesis: for v being VECTOR of Linear_Space_of_ComplexSequences st v in the_set_of_l2ComplexSequences holds
z * v in the_set_of_l2ComplexSequences
let v be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: ( v in the_set_of_l2ComplexSequences implies z * v in the_set_of_l2ComplexSequences )
assume v in the_set_of_l2ComplexSequences ; :: thesis: z * v in the_set_of_l2ComplexSequences
then A12: |.(seq_id v).| (#) |.(seq_id v).| is summable by Def11;
seq_id (z * v) = seq_id (z (#) (seq_id v)) by Th5
.= z (#) (seq_id v) by Th3 ;
then |.(seq_id (z * v)).| = |.z.| (#) |.(seq_id v).| by COMSEQ_1:50;
then |.(seq_id (z * v)).| (#) |.(seq_id (z * v)).| = |.z.| (#) ((|.z.| (#) |.(seq_id v).|) (#) |.(seq_id v).|) by SEQ_1:18
.= |.z.| (#) (|.z.| (#) (|.(seq_id v).| (#) |.(seq_id v).|)) by SEQ_1:18
.= (|.z.| * |.z.|) (#) (|.(seq_id v).| (#) |.(seq_id v).|) by SEQ_1:23 ;
then |.(seq_id (z * v)).| (#) |.(seq_id (z * v)).| is summable by A12, SERIES_1:10;
hence z * v in the_set_of_l2ComplexSequences by Def11; :: thesis: verum

end;

hence ( the_set_of_l2ComplexSequences is linearly-closed & not the_set_of_l2ComplexSequences is empty ) by A1, Def11, CLVECT_1:def 7; :: thesis: verum