set W = the_set_of_l2ComplexSequences ;

hereby :: according to CLVECT_1:def 7 :: thesis: for b₁ being object
for b₂ being Element of the carrier of Linear_Space_of_ComplexSequences holds
( not b₂ in the_set_of_l2ComplexSequences or b₁ * b₂ in the_set_of_l2ComplexSequences )

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
A1: v in the_set_of_l2ComplexSequences and
A2: 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).|;
A3: 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;

A4: 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 t = |.(seq_id u).|;
set s = |.(seq_id v).|;
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
A5: n in NAT by ORDINAL1:def 12;
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: v + u = (seq_id v) + (seq_id u) by Th2;
|.(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, A5 ;
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;
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, XREAL_1:63;
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 A2, Def9;
then A11: 2 (#) (|.(seq_id u).| (#) |.(seq_id u).|) is summable by SERIES_1:10;
|.(seq_id v).| (#) |.(seq_id v).| is summable by A1, Def9;
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 A3, A4, SERIES_1:20; :: thesis: verum

end;

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

end;

let z be Complex; :: thesis: for b₁ being Element of the carrier of Linear_Space_of_ComplexSequences holds
( not b₁ in the_set_of_l2ComplexSequences or z * b₁ in the_set_of_l2ComplexSequences )
let v be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: ( not v in the_set_of_l2ComplexSequences or 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 Def9;
z * v = 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 Def9; :: thesis: verum