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

proof

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

end;

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

proof

let u, v be VECTOR of Complex_linfty_Space; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_BoundedComplexSequences ;
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_BoundedComplexSequences) = [:the_set_of_BoundedComplexSequences,the_set_of_BoundedComplexSequences:] by RELAT_1:62;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_BoundedComplexSequences) . [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 c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)

proof

let c be Complex; :: thesis: for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)
let u be VECTOR of Complex_linfty_Space; :: thesis: c * u = c (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_BoundedComplexSequences ;
reconsider c = c as Element of COMPLEX by XCMPLX_0:def 2;
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_BoundedComplexSequences:]) = [:COMPLEX,the_set_of_BoundedComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
c * u = the Mult of Complex_linfty_Space . [c,u] by CLVECT_1:def 1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_BoundedComplexSequences:]) . [c,u] by CSSPACE:def 9
.= the Mult of Linear_Space_of_ComplexSequences . [c,u] by A5, FUNCT_1:47
.= c * u1 by CLVECT_1:def 1 ;
hence c * u = c (#) (seq_id u) by CSSPACE:3; :: thesis: verum

end;

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

proof

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

end;

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

proof

let u be VECTOR of Complex_linfty_Space; :: thesis: ( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
- u = (- 1r) * u by 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_linfty_Space holds u - v = (seq_id u) - (seq_id v)

proof

let u, v be VECTOR of Complex_linfty_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_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) by Def2;
0. Complex_linfty_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def 10
.= CZeroseq ;
hence ( the carrier of Complex_linfty_Space = the_set_of_BoundedComplexSequences & ( for x being set holds
( x is VECTOR of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) ) ) & 0. Complex_linfty_Space = CZeroseq & ( for u being VECTOR of Complex_linfty_Space holds u = seq_id u ) & ( for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v) ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u) ) & ( for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) ) ) & ( for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v) ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|) ) ) by A1, A6, A2, A4, A7, A8, A9; :: thesis: verum