theorem Th9: :: CSSPACE:14

CLSStruct(# the_set_of_l2ComplexSequences,(Zero_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Add_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)),(Mult_ (the_set_of_l2ComplexSequences,Linear_Space_of_ComplexSequences)) #) is ComplexLinearSpace by Th6;