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 ) )
A2:
for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v)
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;
for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)let u be
VECTOR of
Complex_linfty_Space;
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;
verum
end;
A6:
for u being VECTOR of Complex_linfty_Space holds u = seq_id u
A7:
for u being VECTOR of Complex_linfty_Space holds
( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )
A8:
for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v)
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; verum