set V = Linear_Space_of_RealSequences ;
let p be Real; ( 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
; 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 ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #);
A2:
RLSStruct(# the carrier of lSpacep, the ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #) is Subspace of Linear_Space_of_RealSequences
by A1, Th5;
then A3:
the Mult of lSpacep = the Mult of Linear_Space_of_RealSequences | [:REAL, the carrier of lSpacep:]
by RLSUB_1:def 2;
0. RLSStruct(# the carrier of lSpacep, the ZeroF of lSpacep, the addF of lSpacep, the Mult of lSpacep #) = 0. Linear_Space_of_RealSequences
by A2, RLSUB_1:def 2;
then A4:
0. lSpacep = 0. Linear_Space_of_RealSequences
;
the addF of lSpacep = the addF of Linear_Space_of_RealSequences || the carrier of lSpacep
by A2, RLSUB_1:def 2;
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
by A4, A3, RLSUB_1:def 2; verum