theorem :: CSSPACE4:5

Complex_linfty_Space is ComplexBanachSpace by Th4, CLOPBAN1:def 13;