:: deftheorem Def2 defines seq_id RSSPACE:def 2 :
for a being object st a in the_set_of_RealSequences holds
seq_id a = a;