let p be Real; :: thesis: ( 1 <= p implies RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences )
assume 1 <= p ; :: thesis: RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences
then the_set_of_RealSequences_l^ p is linearly-closed by Th4;
hence RLSStruct(# (the_set_of_RealSequences_l^ p),(Zero_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Add_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ),(Mult_ (the_set_of_RealSequences_l^ p),Linear_Space_of_RealSequences ) #) is Subspace of Linear_Space_of_RealSequences by RSSPACE:13; :: thesis: verum