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:18, RSSPACE:15, 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:91, ZFMISC_1:119;
then A11:
[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 A11, FUNCT_1:70
;
hence
u + v = (seq_id u) + (seq_id v)
by RSSPACE:17;
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:18, RSSPACE:15, 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:91, ZFMISC_1:119;
then A13:
[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 A13, FUNCT_1:70
;
hence
r * u = r (#) (seq_id u)
by RSSPACE:17;
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