theorem Th4: :: CSSPACE3:5

Complex_l1_Space is ComplexLinearSpace by Lm2, CSSPACE:79;