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 ) )

for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)

( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

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

A1: for x being set holds

( x is Element of Complex_linfty_Space iff ( x is Complex_Sequence & seq_id x is bounded ) )

proof

A2:
for u, v being VECTOR of Complex_linfty_Space holds u + v = (seq_id u) + (seq_id v)
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;( 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

proof

A4:
for c being Complex
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;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

for u being VECTOR of Complex_linfty_Space holds c * u = c (#) (seq_id u)

proof

A6:
for u being VECTOR of Complex_linfty_Space holds u = seq_id u
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;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

proof

A7:
for u being VECTOR of Complex_linfty_Space holds
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;u is VECTOR of Linear_Space_of_ComplexSequences by Lm5, CLVECT_1:29;

hence u = seq_id u ; :: thesis: verum

( - u = - (seq_id u) & seq_id (- u) = - (seq_id u) )

proof

A8:
for u, v being VECTOR of Complex_linfty_Space holds u - v = (seq_id u) - (seq_id v)
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;- 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

proof

A9:
for v being VECTOR of Complex_linfty_Space holds ||.v.|| = upper_bound (rng |.(seq_id v).|)
by Def2;
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;thus u - v = (seq_id u) + (seq_id (- v)) by A2

.= (seq_id u) - (seq_id v) by A7 ; :: thesis: verum

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