let p be Real; :: thesis: ( p >= 1 implies NORMSTR(# (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 ),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences )
assume A1: 1 <= p ; :: thesis: NORMSTR(# (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 ),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences
set lSpacep = NORMSTR(# (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 ),(l_norm^ p) #);
reconsider lSpacep = NORMSTR(# (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 ),(l_norm^ p) #) as RealLinearSpace by A1, Th8;
set w1 = RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #);
set V = Linear_Space_of_RealSequences ;
A2: RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) is Subspace of Linear_Space_of_RealSequences by A1, Th5;
then A3: ( the carrier of RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) c= the carrier of Linear_Space_of_RealSequences & 0. RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) = 0. Linear_Space_of_RealSequences & the addF of RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) = the addF of Linear_Space_of_RealSequences || the carrier of RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) & the Mult of RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #) = the Mult of Linear_Space_of_RealSequences | [:REAL ,the carrier of RLSStruct(# the carrier of lSpacep,the U2 of lSpacep,the addF of lSpacep,the Mult of lSpacep #):] ) by RLSUB_1:def 2;
lSpacep is Subspace of Linear_Space_of_RealSequences

proof

thus the carrier of lSpacep c= the carrier of Linear_Space_of_RealSequences ; :: according to RLSUB_1:def 2 :: thesis: ( 0. lSpacep = 0. Linear_Space_of_RealSequences & the addF of lSpacep = the addF of Linear_Space_of_RealSequences || the carrier of lSpacep & the Mult of lSpacep = the Mult of Linear_Space_of_RealSequences | [:REAL ,the carrier of lSpacep:] )
thus 0. lSpacep = 0. Linear_Space_of_RealSequences by A3; :: thesis: ( the addF of lSpacep = the addF of Linear_Space_of_RealSequences || the carrier of lSpacep & the Mult of lSpacep = the Mult of Linear_Space_of_RealSequences | [:REAL ,the carrier of lSpacep:] )
thus ( the addF of lSpacep = the addF of Linear_Space_of_RealSequences || the carrier of lSpacep & the Mult of lSpacep = the Mult of Linear_Space_of_RealSequences | [:REAL ,the carrier of lSpacep:] ) by A2, RLSUB_1:def 2; :: thesis: verum

end;

hence NORMSTR(# (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 ),(l_norm^ p) #) is Subspace of Linear_Space_of_RealSequences ; :: thesis: verum