for p being Real st 1 <= p holds
the_set_of_RealSequences_l^ p is linearly-closed