A1: for x being set holds
( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) )

proof

let x be set ; :: thesis: ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) )
( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def 1;
hence ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) by RSSPACE:def 11, RSSPACE:def 13; :: thesis: verum

end;

A2: for u being VECTOR of l2_Space holds u = seq_id u

proof

let u be VECTOR of l2_Space ; :: thesis: u = seq_id u
u is VECTOR of Linear_Space_of_RealSequences by RLSUB_1:18, RSSPACE:15, RSSPACE:def 13;
hence u = seq_id u by RSSPACE:17; :: thesis: verum

end;

A3: for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v)

proof

let u, v be VECTOR of l2_Space ; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:18, RSSPACE:15, RSSPACE:def 13;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l2RealSequences ;
dom the addF of Linear_Space_of_RealSequences = [:the carrier of Linear_Space_of_RealSequences ,the carrier of Linear_Space_of_RealSequences :] by FUNCT_2:def 1;
then dom (the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences ) = [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :] by RELAT_1:91, ZFMISC_1:119;
then A4: [u,v] in dom (the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences ) by RSSPACE:def 13, ZFMISC_1:106;
u + v = (the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences ) . [u,v] by RSSPACE:def 8, RSSPACE:def 13
.= u1 + v1 by A4, FUNCT_1:70 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:17; :: thesis: verum

end;

A5: for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)

proof

let r be Real; :: thesis: for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of l2_Space ; :: thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:18, RSSPACE:15, RSSPACE:def 13;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_l2RealSequences ;
dom the Mult of Linear_Space_of_RealSequences = [:REAL ,the carrier of Linear_Space_of_RealSequences :] by FUNCT_2:def 1;
then dom (the Mult of Linear_Space_of_RealSequences | [:REAL ,the_set_of_l2RealSequences :]) = [:REAL ,the_set_of_l2RealSequences :] by RELAT_1:91, ZFMISC_1:119;
then A6: [r,u] in dom (the Mult of Linear_Space_of_RealSequences | [:REAL ,the_set_of_l2RealSequences :]) by RSSPACE:def 13, ZFMISC_1:106;
r * u = (the Mult of Linear_Space_of_RealSequences | [:REAL ,the_set_of_l2RealSequences :]) . [r,u] by RSSPACE:def 9, RSSPACE:def 13
.= r * u1 by A6, FUNCT_1:70 ;
hence r * u = r (#) (seq_id u) by RSSPACE:17; :: thesis: verum

end;

A7: for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

proof

let u be VECTOR of l2_Space ; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1) * u by RLVECT_1:29
.= (- 1) (#) (seq_id u) by A5
.= - (seq_id u) by SEQ_1:25 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) by A2; :: thesis: verum

end;

A8: for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v)

proof

let u, v be VECTOR of l2_Space ; :: thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A3
.= (seq_id u) + (- (seq_id v)) by A7
.= (seq_id u) - (seq_id v) by SEQ_1:15 ; :: thesis: verum

end;

A9: 0. l2_Space = Zeroseq

proof

thus 0. l2_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def 10, RSSPACE:def 13
.= Zeroseq by RSSPACE:def 7 ; :: thesis: verum

end;

A10: for u, v being VECTOR of l2_Space holds (seq_id u) (#) (seq_id v) is summable

proof

let u, v be VECTOR of l2_Space ; :: thesis: (seq_id u) (#) (seq_id v) is summable
A11: (seq_id v) (#) (seq_id v) is summable by RSSPACE:def 11, RSSPACE:def 13;
A12: (seq_id u) (#) (seq_id u) is summable by RSSPACE:def 11, RSSPACE:def 13;
set p = (seq_id v) (#) (seq_id v);
set q = (seq_id u) (#) (seq_id u);
set r = abs ((seq_id u) (#) (seq_id v));
A13: ((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u)) is summable by A11, A12, SERIES_1:10;
A14: for n being Element of NAT holds 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

proof

let n be Element of NAT ; :: thesis: 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n
set rr = (seq_id u) (#) (seq_id v);
A15: (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n = 2 * ((abs ((seq_id u) (#) (seq_id v))) . n) by SEQ_1:13
.= 2 * (abs (((seq_id u) (#) (seq_id v)) . n)) by SEQ_1:16 ;
reconsider tt = abs (((seq_id u) (#) (seq_id v)) . n) as Real ;
( 0 <= 2 & 0 <= tt ) by COMPLEX1:132;
hence 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n by A15; :: thesis: verum

end;

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

proof

let n be Element of NAT ; :: thesis: (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n <= (((seq_id v) (#) (seq_id v)) + ((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 ;
reconsider ss = abs sn, tt = abs tn as Real ;
A16: (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n = 2 * ((abs ((seq_id u) (#) (seq_id v))) . n) by SEQ_1:13
.= 2 * (abs (((seq_id u) (#) (seq_id v)) . n)) by SEQ_1:16
.= 2 * (abs (((seq_id u) . n) * ((seq_id v) . n))) by SEQ_1:12
.= 2 * (ss * tt) by COMPLEX1:151
.= (2 * (abs sn)) * (abs tn) ;
A17: (((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u))) . n = (((seq_id v) (#) (seq_id v)) . n) + (((seq_id u) (#) (seq_id u)) . n) by SEQ_1:11
.= (((seq_id v) . n) * ((seq_id v) . n)) + (((seq_id u) (#) (seq_id u)) . n) by SEQ_1:12
.= (sn ^2 ) + (((seq_id u) . n) * ((seq_id u) . n)) by SEQ_1:12
.= ((abs sn) ^2 ) + (tn ^2 ) by COMPLEX1:161
.= ((abs sn) ^2 ) + ((abs tn) ^2 ) by COMPLEX1:161 ;
0 <= ((abs sn) - (abs tn)) ^2 by XREAL_1:65;
then 0 + ((2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n) <= (((((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u))) . n) - ((2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n)) + ((2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n) by A16, A17, XREAL_1:9;
hence (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n <= (((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u))) . n ; :: thesis: verum

end;

then A18: 2 (#) (abs ((seq_id u) (#) (seq_id v))) is summable by A13, A14, SERIES_1:24;
set q0 = 1 / 2;
(1 / 2) (#) (2 (#) (abs ((seq_id u) (#) (seq_id v)))) = ((1 / 2) * 2) (#) (abs ((seq_id u) (#) (seq_id v))) by SEQ_1:31
.= abs ((seq_id u) (#) (seq_id v)) by SEQ_1:35 ;
then abs ((seq_id u) (#) (seq_id v)) is summable by A18, SERIES_1:13;
then (seq_id u) (#) (seq_id v) is absolutely_summable by SERIES_1:def 5;
hence (seq_id u) (#) (seq_id v) is summable by SERIES_1:40; :: thesis: verum

end;

for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))

proof

let v, w be VECTOR of l2_Space ; :: thesis: v .|. w = Sum ((seq_id v) (#) (seq_id w))
thus v .|. w = the scalar of l2_Space . v,w by BHSP_1:def 1
.= Sum ((seq_id v) (#) (seq_id w)) by RSSPACE:def 12, RSSPACE:def 13 ; :: thesis: verum

end;

hence ( the carrier of l2_Space = the_set_of_l2RealSequences & ( for x being set holds
( x is VECTOR of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) ) & 0. l2_Space = Zeroseq & ( for u being VECTOR of l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of l2_Space holds
( (seq_id v) (#) (seq_id w) is summable & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w)) ) ) ) ) by A1, A2, A3, A5, A7, A8, A9, A10, RSSPACE:def 13; :: thesis: verum