theorem :: CSSPACE2:1

( the carrier of Complex_l2_Space = the_set_of_l2ComplexSequences & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & |.(seq_id x).| (#) |.(seq_id x).| is summable ) ) ) & ( for x being set holds
( x is Element of Complex_l2_Space iff ( x is Complex_Sequence & (seq_id x) (#) ((seq_id x) *') is absolutely_summable ) ) ) & 0. Complex_l2_Space = CZeroseq & ( for u being VECTOR of Complex_l2_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l2_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for r being Complex
for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u) ) & ( for u being VECTOR of Complex_l2_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l2_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v, w being VECTOR of Complex_l2_Space holds
( |.(seq_id v).| (#) |.(seq_id w).| is summable & ( for v, w being VECTOR of Complex_l2_Space holds v .|. w = Sum ((seq_id v) (#) ((seq_id w) *')) ) ) ) ) by Lm9, Lm10, Lm12, Lm13, Lm14, Lm15, Lm16, Lm19, CSSPACE:def 17;