theorem Th4: :: LP_SPACE:4

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