let p be Real; :: thesis:
assume A1: 1 <= p ; :: thesis:
let lp be non empty NORMSTR ; :: thesis:
assume A2: lp = 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) #) ; :: thesis:
A3: for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3;
A4: for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y)

proof

let x, y be VECTOR of lp; :: thesis:
A5: lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:18;
reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by A5, RLSUB_1:18;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_RealSequences_l^ p;
dom the addF of Linear_Space_of_RealSequences = [: the carrier of Linear_Space_of_RealSequences, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;
then A6: dom ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) = [:(the_set_of_RealSequences_l^ p),(the_set_of_RealSequences_l^ p):] by RELAT_1:91;
the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then x + y = ( the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) . [x,y] by A2, RSSPACE:def 8
.= x1 + y1 by A2, A6, FUNCT_1:70 ;
hence x + y = (seq_id x) + (seq_id y) by RSSPACE:4, RSSPACE:def 7; :: thesis:

end;

A7: for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x)

proof

set W = the_set_of_RealSequences_l^ p;
set L1 = Linear_Space_of_RealSequences ;
let r be Real; :: thesis:
let x be VECTOR of lp; :: thesis:
dom the Mult of Linear_Space_of_RealSequences = [:REAL, the carrier of Linear_Space_of_RealSequences:] by FUNCT_2:def 1;
then A8: dom ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) = [:REAL,(the_set_of_RealSequences_l^ p):] by RELAT_1:91, ZFMISC_1:119;
lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then reconsider x1 = x as VECTOR of Linear_Space_of_RealSequences by RLSUB_1:18;
the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then r * x = ( the Mult of Linear_Space_of_RealSequences | [:REAL,(the_set_of_RealSequences_l^ p):]) . [r,x] by A2, RSSPACE:def 9
.= r * x1 by A2, A8, FUNCT_1:70 ;
hence r * x = r (#) (seq_id x) by RSSPACE:5, RSSPACE:def 7; :: thesis:

end;

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
then A9: 0. lp = 0. Linear_Space_of_RealSequences by A2, RSSPACE:def 10
.= Zeroseq by RSSPACE:def 7 ;
A10: for x being set holds
( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )

proof

let x be set ; :: thesis:
( x in the_set_of_RealSequences_l^ p iff ( (seq_id x) rto_power p is summable & x in the_set_of_RealSequences ) ) by A1, Def2;
hence ( x is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) by A2, RSSPACE:def 1; :: thesis:

end;

A11: for x being set st x is VECTOR of lp holds
x = seq_id x

proof

let x be set ; :: thesis:
( x in the_set_of_RealSequences iff x is Real_Sequence ) by RSSPACE:def 1;
hence ( x is VECTOR of lp implies x = seq_id x ) by A1, A2, Def2, RSSPACE:3; :: thesis:

end;

A12: for x being VECTOR of lp holds
( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )

proof

let x be VECTOR of lp; :: thesis:
lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then - x = (- 1) * x by RLVECT_1:29
.= - (seq_id x) by A7 ;
hence ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) by A11; :: thesis:

end;

for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y)

proof

let x, y be VECTOR of lp; :: thesis:
thus x - y = (seq_id x) + (seq_id (- y)) by A4
.= (seq_id x) - (seq_id y) by A12 ; :: thesis:

end;

hence ( the carrier of lp = the_set_of_RealSequences_l^ p & ( for x being set holds
( x is VECTOR of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) ) ) & 0. lp = Zeroseq & ( for x being VECTOR of lp holds x = seq_id x ) & ( for x, y being VECTOR of lp holds x + y = (seq_id x) + (seq_id y) ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) (seq_id x) ) & ( for x being VECTOR of lp holds
( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) ) & ( for x, y being VECTOR of lp holds x - y = (seq_id x) - (seq_id y) ) & ( for x being VECTOR of lp holds (seq_id x) rto_power p is summable ) & ( for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ) ) by A2, A10, A11, A9, A4, A7, A12, A3; :: thesis: