:: deftheorem defines Linear_Space_of_ComplexSequences CSSPACE:def 7 :
Linear_Space_of_ComplexSequences = ComplexVectSpace NAT;