( the carrier of Complex_l1_Space = the_set_of_l1ComplexSequences & ( for x being set holds
( x is VECTOR of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) ) & 0. Complex_l1_Space = CZeroseq & ( for u being VECTOR of Complex_l1_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u) ) & ( for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_l1_Space holds seq_id v is absolutely_summable ) & ( for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| ) )