let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st 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) #) holds
( 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) ) ) )
assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st 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) #) holds
( 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) ) )
let lp be non empty NORMSTR ; :: thesis: ( 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) #) implies ( 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) ) ) )
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: ( 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) ) )
A3: 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 is Element of lp iff ( x is Real_Sequence & (seq_id x) rto_power p is summable ) )
( 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: verum

end;

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

proof

let x be set ; :: thesis: ( x is VECTOR of lp implies x = seq_id x )
( 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: verum

end;

A5: 0. lp = Zeroseq

proof

the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
hence 0. lp = 0. Linear_Space_of_RealSequences by A2, RSSPACE:def 10
.= Zeroseq by RSSPACE:def 7 ;
:: thesis: verum

end;

A6: 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: x + y = (seq_id x) + (seq_id y)
A7: 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 A7, RLSUB_1:18;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_RealSequences_l^ p;
A8: the_set_of_RealSequences_l^ p is linearly-closed by A1, Th4;
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 A9: 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;
x + y = (the addF of Linear_Space_of_RealSequences || (the_set_of_RealSequences_l^ p)) . [x,y] by A2, A8, RSSPACE:def 8
.= x1 + y1 by A2, A9, FUNCT_1:70 ;
hence x + y = (seq_id x) + (seq_id y) by RSSPACE:4, RSSPACE:def 7; :: thesis: verum

end;

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

proof

let r be Real; :: thesis: for x being VECTOR of lp holds r * x = r (#) (seq_id x)
let x be VECTOR of lp; :: thesis: r * x = r (#) (seq_id x)
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;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_RealSequences_l^ p;
dom the Mult of Linear_Space_of_RealSequences = [:REAL ,the carrier of Linear_Space_of_RealSequences :] by FUNCT_2:def 1;
then A11: 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;
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, A11, FUNCT_1:70 ;
hence r * x = r (#) (seq_id x) by RSSPACE:5, RSSPACE:def 7; :: thesis: verum

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: ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) )
lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then - x = (- 1) * x by RLVECT_1:29
.= - (seq_id x) by A10 ;
hence ( - x = - (seq_id x) & seq_id (- x) = - (seq_id x) ) by A4; :: thesis: verum

end;

A13: 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: x - y = (seq_id x) - (seq_id y)
thus x - y = (seq_id x) + (seq_id (- y)) by A6
.= (seq_id x) - (seq_id y) by A12 ; :: thesis: verum

end;

for x being VECTOR of lp holds ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p)

proof

let x be VECTOR of lp; :: thesis: ||.x.|| = (Sum ((seq_id x) rto_power p)) to_power (1 / p)
thus ||.x.|| = the norm of lp . x by NORMSP_1:def 1
.= (Sum ((seq_id x) rto_power p)) to_power (1 / p) by A2, Def3 ; :: thesis: verum

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, A3, A4, A5, A6, A10, A12, A13; :: thesis: verum