:: deftheorem defines the_set_of_RealSequences RSSPACE:def 1 :
the_set_of_RealSequences = Funcs (NAT,REAL);