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 & () (#) () 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 = () + () ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () ) & ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )

thus for x being set holds
( x is Element of l2_Space iff ( x is Real_Sequence & () (#) () 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 = () + () ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () ) & ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )
proof
let x be set ; :: thesis: ( x is Element of l2_Space iff ( x is Real_Sequence & () (#) () is summable ) )
( x in the_set_of_RealSequences iff x is Real_Sequence ) by ;
hence ( x is Element of l2_Space iff ( x is Real_Sequence & () (#) () 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 = () + () ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () ) & ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )

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 = () + () ) & ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () ) & ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )

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 = () + () :: thesis: ( ( for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () ) & ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )
proof
let u, v be VECTOR of l2_Space; :: thesis: u + v = () + ()
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_RealSequences by ;
dom the addF of Linear_Space_of_RealSequences = by FUNCT_2:def 1;
then dom = by ;
then A11: [u,v] in dom by ZFMISC_1:87;
u + v = . [u,v] by RSSPACE:def 8
.= u1 + v1 by ;
hence u + v = () + () by RSSPACE:2; :: thesis: verum
end;
thus A12: for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) () :: thesis: ( ( for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) ) & ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )
proof
let r be Real; :: thesis: for u being VECTOR of l2_Space holds r * u = r (#) ()
reconsider r = r as Element of REAL by XREAL_0:def 1;
let u be VECTOR of l2_Space; :: thesis: r * u = r (#) ()
reconsider u1 = u as VECTOR of Linear_Space_of_RealSequences by ;
dom the Mult of Linear_Space_of_RealSequences = by FUNCT_2:def 1;
then dom = by ;
then A13: [r,u] in dom by ZFMISC_1:87;
r * u = . [r,u] by RSSPACE:def 9
.= r * u1 by ;
hence r * u = r (#) () by RSSPACE:3; :: thesis: verum
end;
thus A15: for u being VECTOR of l2_Space holds
( - u = - () & seq_id (- u) = - () ) :: thesis: ( ( for u, v being VECTOR of l2_Space holds u - v = () - () ) & ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )
proof
let u be VECTOR of l2_Space; :: thesis: ( - u = - () & seq_id (- u) = - () )
- u = (- 1) * u by RLVECT_1:16
.= (- 1) (#) () by A12
.= - () by SEQ_1:17 ;
hence ( - u = - () & seq_id (- u) = - () ) ; :: thesis: verum
end;
thus for u, v being VECTOR of l2_Space holds u - v = () - () :: thesis: ( ( for v, w being VECTOR of l2_Space holds () (#) () is summable ) & ( for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) ) )
proof
let u, v be VECTOR of l2_Space; :: thesis: u - v = () - ()
thus u - v = () + (seq_id (- v)) by A10
.= () + (- ()) by A15
.= () - () by SEQ_1:11 ; :: thesis: verum
end;
thus for u, v being VECTOR of l2_Space holds () (#) () is summable :: thesis: for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ())
proof
set q0 = 1 / 2;
let u, v be VECTOR of l2_Space; :: thesis: () (#) () is summable
set p = () (#) ();
set q = () (#) ();
set r = abs (() (#) ());
A2: for n being Nat holds 0 <= (2 (#) (abs (() (#) ()))) . n
proof
set rr = () (#) ();
let n be Nat; :: thesis: 0 <= (2 (#) (abs (() (#) ()))) . n
reconsider tt = |.((() (#) ()) . n).| as Real ;
A3: 0 <= tt by COMPLEX1:46;
(2 (#) (abs (() (#) ()))) . n = 2 * ((abs (() (#) ())) . n) by SEQ_1:9
.= 2 * |.((() (#) ()) . n).| by SEQ_1:12 ;
hence 0 <= (2 (#) (abs (() (#) ()))) . n by A3; :: thesis: verum
end;
A4: for n being Nat holds (2 (#) (abs (() (#) ()))) . n <= ((() (#) ()) + (() (#) ())) . n
proof
set s = seq_id v;
set t = seq_id u;
let n be Nat; :: thesis: (2 (#) (abs (() (#) ()))) . n <= ((() (#) ()) + (() (#) ())) . n
reconsider sn = () . n, tn = () . n as Real ;
reconsider ss = |.sn.|, tt = |.tn.| as Real ;
A5: ((() (#) ()) + (() (#) ())) . n = ((() (#) ()) . n) + ((() (#) ()) . n) by SEQ_1:7
.= ((() . n) * (() . n)) + ((() (#) ()) . n) by SEQ_1:8
.= (sn ^2) + ((() . n) * (() . 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 (() (#) ()))) . n = 2 * ((abs (() (#) ())) . n) by SEQ_1:9
.= 2 * |.((() (#) ()) . n).| by SEQ_1:12
.= 2 * |.((() . n) * (() . n)).| by SEQ_1:8
.= 2 * (ss * tt) by COMPLEX1:65
.= (2 * |.sn.|) * |.tn.| ;
then 0 + ((2 (#) (abs (() (#) ()))) . n) <= ((((() (#) ()) + (() (#) ())) . n) - ((2 (#) (abs (() (#) ()))) . n)) + ((2 (#) (abs (() (#) ()))) . n) by ;
hence (2 (#) (abs (() (#) ()))) . n <= ((() (#) ()) + (() (#) ())) . n ; :: thesis: verum
end;
A7: (1 / 2) (#) (2 (#) (abs (() (#) ()))) = ((1 / 2) * 2) (#) (abs (() (#) ())) by SEQ_1:23
.= abs (() (#) ()) by SEQ_1:27 ;
( (seq_id v) (#) () is summable & () (#) () is summable ) by RSSPACE:def 11;
then ((seq_id v) (#) ()) + (() (#) ()) is summable by SERIES_1:7;
then 2 (#) (abs (() (#) ())) is summable by ;
then abs (() (#) ()) is summable by ;
then (seq_id u) (#) () is absolutely_summable by SERIES_1:def 4;
hence (seq_id u) (#) () is summable ; :: thesis: verum
end;
thus for v, w being VECTOR of l2_Space holds v .|. w = Sum (() (#) ()) :: thesis: verum
proof
let v, w be VECTOR of l2_Space; :: thesis: v .|. w = Sum (() (#) ())
thus v .|. w = the scalar of l2_Space . (v,w) by BHSP_1:def 1
.= Sum (() (#) ()) by RSSPACE:def 12 ; :: thesis: verum
end;