thus the carrier of l2_Space = the_set_of_l2RealSequences ; :: thesis: ( ( 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)) ) )
thus for x being set holds
( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) :: thesis: ( 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)) ) )

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 FUNCT_2:8, FUNCT_2:66;
hence ( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) ) by RSSPACE:def 11; :: thesis: verum

end;

thus 0. l2_Space = 0. Linear_Space_of_RealSequences by RSSPACE:def 10
.= Zeroseq ; :: thesis: ( ( 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)) ) )
thus for u being VECTOR of l2_Space holds u = seq_id u ; :: thesis: ( ( 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)) ) )
set W = the_set_of_l2RealSequences ;
set L1 = Linear_Space_of_RealSequences ;
thus A10: for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v) :: thesis: ( ( 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)) ) )

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:10, RSSPACE:12;
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:62, ZFMISC_1:96;
then A11: [u,v] in dom ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) by ZFMISC_1:87;
u + v = ( the addF of Linear_Space_of_RealSequences || the_set_of_l2RealSequences) . [u,v] by RSSPACE:def 8
.= u1 + v1 by A11, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by RSSPACE:2; :: thesis: verum

end;

thus A12: for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u) :: thesis: ( ( 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)) ) )

proof

let r be Real; :: thesis: for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)
reconsider r = r as Element of REAL by XREAL_0:def 1;
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:10, RSSPACE:12;
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:62, ZFMISC_1:96;
then A13: [r,u] in dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) by ZFMISC_1:87;
r * u = ( the Mult of Linear_Space_of_RealSequences | [:REAL,the_set_of_l2RealSequences:]) . [r,u] by RSSPACE:def 9
.= r * u1 by A13, FUNCT_1:47 ;
hence r * u = r (#) (seq_id u) by RSSPACE:3; :: thesis: verum

end;

thus A15: for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) :: thesis: ( ( 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)) ) )

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:16
.= (- 1) (#) (seq_id u) by A12
.= - (seq_id u) by SEQ_1:17 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ; :: thesis: verum

end;

thus for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v) :: thesis: ( ( 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)) ) )

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 A10
.= (seq_id u) + (- (seq_id v)) by A15
.= (seq_id u) - (seq_id v) by SEQ_1:11 ; :: thesis: verum

end;

thus for u, v being VECTOR of l2_Space holds (seq_id u) (#) (seq_id v) is summable :: thesis: for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))

proof

set q0 = 1 / 2;
let u, v be VECTOR of l2_Space; :: thesis: (seq_id u) (#) (seq_id v) is summable
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));
A2: for n being Nat holds 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n

proof

set rr = (seq_id u) (#) (seq_id v);
let n be Nat; :: thesis: 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n
reconsider tt = |.(((seq_id u) (#) (seq_id v)) . n).| as Real ;
A3: 0 <= tt by COMPLEX1:46;
(2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n = 2 * ((abs ((seq_id u) (#) (seq_id v))) . n) by SEQ_1:9
.= 2 * |.(((seq_id u) (#) (seq_id v)) . n).| by SEQ_1:12 ;
hence 0 <= (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n by A3; :: thesis: verum

end;

A4: for n being 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

set s = seq_id v;
set t = seq_id u;
let n be Nat; :: thesis: (2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n <= (((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u))) . n
reconsider sn = (seq_id v) . n, tn = (seq_id u) . n as Real ;
reconsider ss = |.sn.|, tt = |.tn.| as Real ;
A5: (((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:7
.= (((seq_id v) . n) * ((seq_id v) . n)) + (((seq_id u) (#) (seq_id u)) . n) by SEQ_1:8
.= (sn ^2) + (((seq_id u) . n) * ((seq_id u) . n)) by SEQ_1:8
.= (|.sn.| ^2) + (tn ^2) by COMPLEX1:75
.= (|.sn.| ^2) + (|.tn.| ^2) by COMPLEX1:75 ;
A6: 0 <= (|.sn.| - |.tn.|) ^2 by XREAL_1:63;
(2 (#) (abs ((seq_id u) (#) (seq_id v)))) . n = 2 * ((abs ((seq_id u) (#) (seq_id v))) . n) by SEQ_1:9
.= 2 * |.(((seq_id u) (#) (seq_id v)) . n).| by SEQ_1:12
.= 2 * |.(((seq_id u) . n) * ((seq_id v) . n)).| by SEQ_1:8
.= 2 * (ss * tt) by COMPLEX1:65
.= (2 * |.sn.|) * |.tn.| ;
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 A5, A6, XREAL_1:7;
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;

A7: (1 / 2) (#) (2 (#) (abs ((seq_id u) (#) (seq_id v)))) = ((1 / 2) * 2) (#) (abs ((seq_id u) (#) (seq_id v))) by SEQ_1:23
.= abs ((seq_id u) (#) (seq_id v)) by SEQ_1:27 ;
( (seq_id v) (#) (seq_id v) is summable & (seq_id u) (#) (seq_id u) is summable ) by RSSPACE:def 11;
then ((seq_id v) (#) (seq_id v)) + ((seq_id u) (#) (seq_id u)) is summable by SERIES_1:7;
then 2 (#) (abs ((seq_id u) (#) (seq_id v))) is summable by A2, A4, SERIES_1:20;
then abs ((seq_id u) (#) (seq_id v)) is summable by A7, SERIES_1:10;
then (seq_id u) (#) (seq_id v) is absolutely_summable by SERIES_1:def 4;
hence (seq_id u) (#) (seq_id v) is summable ; :: thesis: verum

end;

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

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 ; :: thesis: verum

end;