A1:
for u, v being VECTOR of l2_Space holds (seq_id u) (#) (seq_id v) is summable
A8:
for x being set holds
( x is Element of l2_Space iff ( x is Real_Sequence & (seq_id x) (#) (seq_id x) is summable ) )
A9:
for v, w being VECTOR of l2_Space holds v .|. w = Sum ((seq_id v) (#) (seq_id w))
A10:
for u, v being VECTOR of l2_Space holds u + v = (seq_id u) + (seq_id v)
proof
set W =
the_set_of_l2RealSequences ;
set L1 =
Linear_Space_of_RealSequences ;
let u,
v be
VECTOR of
l2_Space;
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, RSSPACE:def 13;
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 RSSPACE:def 13, ZFMISC_1:87;
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 A11, FUNCT_1:47
;
hence
u + v = (seq_id u) + (seq_id v)
by RSSPACE:14;
verum
end;
A12:
for r being Real
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)
proof
set W =
the_set_of_l2RealSequences ;
set L1 =
Linear_Space_of_RealSequences ;
let r be
Real;
for u being VECTOR of l2_Space holds r * u = r (#) (seq_id u)let u be
VECTOR of
l2_Space;
r * u = r (#) (seq_id u)
reconsider u1 =
u as
VECTOR of
Linear_Space_of_RealSequences by RLSUB_1:10, RSSPACE:12, RSSPACE:def 13;
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 RSSPACE:def 13, ZFMISC_1:87;
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 A13, FUNCT_1:47
;
hence
r * u = r (#) (seq_id u)
by RSSPACE:14;
verum
end;
A14:
for u being VECTOR of l2_Space holds u = seq_id u
A15:
for u being VECTOR of l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
A16:
for u, v being VECTOR of l2_Space holds u - v = (seq_id u) - (seq_id v)
0. l2_Space =
0. Linear_Space_of_RealSequences
by RSSPACE:def 10, RSSPACE:def 13
.=
Zeroseq
by RSSPACE:def 7
;
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 A8, A14, A10, A12, A15, A16, A1, A9, RSSPACE:def 13; verum