:: deftheorem defines the_set_of_ComplexSequences CSSPACE:def 1 :
the_set_of_ComplexSequences = Funcs (NAT,COMPLEX);