:: deftheorem Def2 defines seq_id CSSPACE:def 2 :
for z being object st z in the_set_of_ComplexSequences holds
seq_id z = z;