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 end;
A2: for u, v being VECTOR of Complex_linfty_Space holds u + v = () + ()
proof end;
A4: for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) ()
proof end;
A6: for u being VECTOR of Complex_linfty_Space holds u = seq_id u
proof end;
A7: 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 = () * u by CLVECT_1:3
.= () (#) () by A4
.= - () by COMSEQ_1:11 ;
hence ( - u = - () & seq_id (- u) = - () ) ; :: thesis: verum
end;
A8: for u, v being VECTOR of Complex_linfty_Space holds u - v = () - ()
proof
let u, v be VECTOR of Complex_linfty_Space; :: thesis: u - v = () - ()
thus u - v = () + (seq_id (- v)) by A2
.= () - () by A7 ; :: thesis: verum
end;
A9: for v being VECTOR of Complex_linfty_Space holds = upper_bound (rng |.().|) 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 = () + () ) & ( for c being Complex
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) () ) & ( 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 = () - () ) & ( for v being VECTOR of Complex_linfty_Space holds seq_id v is bounded ) & ( for v being VECTOR of Complex_linfty_Space holds = upper_bound (rng |.().|) ) ) by A1, A6, A2, A4, A7, A8, A9; :: thesis: verum