set l1 = Complex_l1_Space ;
A1: for x being set holds
( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) )

proof

let x be set ; :: thesis: ( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) )
( x in the_set_of_ComplexSequences iff x is Complex_Sequence ) by FUNCT_2:8, FUNCT_2:66;
hence ( x is Element of Complex_l1_Space iff ( x is Complex_Sequence & seq_id x is absolutely_summable ) ) by Def1; :: thesis: verum

end;

A2: for u, v being VECTOR of Complex_l1_Space holds u + v = (seq_id u) + (seq_id v)

proof

let u, v be VECTOR of Complex_l1_Space; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_l1ComplexSequences ;
dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def 1;
then A3: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l1ComplexSequences) = [:the_set_of_l1ComplexSequences,the_set_of_l1ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l1ComplexSequences) . [u,v] by CSSPACE:def 8
.= u1 + v1 by A3, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by CSSPACE:2; :: thesis: verum

end;

A4: for p being Complex
for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u)

proof

let p be Complex; :: thesis: for u being VECTOR of Complex_l1_Space holds p * u = p (#) (seq_id u)
let u be VECTOR of Complex_l1_Space; :: thesis: p * u = p (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_l1ComplexSequences ;
dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def 1;
then A5: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l1ComplexSequences:]) = [:COMPLEX,the_set_of_l1ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
reconsider p = p as Element of COMPLEX by XCMPLX_0:def 2;
p * u = the Mult of Complex_l1_Space . [p,u] by CLVECT_1:def 1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l1ComplexSequences:]) . [p,u] by CSSPACE:def 9
.= the Mult of Linear_Space_of_ComplexSequences . [p,u] by A5, FUNCT_1:47
.= p * u1 by CLVECT_1:def 1 ;
hence p * u = p (#) (seq_id u) by CSSPACE:3; :: thesis: verum

end;

A6: for u being VECTOR of Complex_l1_Space holds u = seq_id u

proof

let u be VECTOR of Complex_l1_Space; :: thesis: u = seq_id u
u is VECTOR of Linear_Space_of_ComplexSequences by Lm1, CLVECT_1:29;
hence u = seq_id u ; :: thesis: verum

end;

A7: for u being VECTOR of Complex_l1_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

proof

let u be VECTOR of Complex_l1_Space; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r) * u by Th4, CLVECT_1:3
.= (- 1r) (#) (seq_id u) by A4
.= - (seq_id u) by COMSEQ_1:11 ;
hence ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ; :: thesis: verum

end;

A8: for u, v being VECTOR of Complex_l1_Space holds u - v = (seq_id u) - (seq_id v)

proof

let u, v be VECTOR of Complex_l1_Space; :: thesis: u - v = (seq_id u) - (seq_id v)
thus u - v = (seq_id u) + (seq_id (- v)) by A2
.= (seq_id u) - (seq_id v) by A7 ; :: thesis: verum

end;

A9: for v being VECTOR of Complex_l1_Space holds ||.v.|| = Sum |.(seq_id v).| by Def2;
0. Complex_l1_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def 10
.= CZeroseq ;
hence ( 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).| ) ) by A1, A6, A2, A4, A7, A8, A9; :: thesis: verum