let p be Real; :: thesis: ( 1 <= p implies for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) 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 & () 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 = () + () ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) () ) & ( for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () ) ) & ( for x, y being VECTOR of lp holds x - y = () - () ) & ( for x being VECTOR of lp holds () rto_power p is summable ) & ( for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) ) ) )

assume A1: 1 <= p ; :: thesis: for lp being non empty NORMSTR st lp = NORMSTR(# ,,,,() #) 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 & () 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 = () + () ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) () ) & ( for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () ) ) & ( for x, y being VECTOR of lp holds x - y = () - () ) & ( for x being VECTOR of lp holds () rto_power p is summable ) & ( for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) ) )

let lp be non empty NORMSTR ; :: thesis: ( lp = NORMSTR(# ,,,,() #) 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 & () 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 = () + () ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) () ) & ( for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () ) ) & ( for x, y being VECTOR of lp holds x - y = () - () ) & ( for x being VECTOR of lp holds () rto_power p is summable ) & ( for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) ) ) )

assume A2: lp = NORMSTR(# ,,,,() #) ; :: 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 & () 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 = () + () ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) () ) & ( for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () ) ) & ( for x, y being VECTOR of lp holds x - y = () - () ) & ( for x being VECTOR of lp holds () rto_power p is summable ) & ( for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) ) )

A3: for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) by ;
A4: for x, y being VECTOR of lp holds x + y = () + ()
proof
let x, y be VECTOR of lp; :: thesis: x + y = () + ()
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:10;
reconsider y1 = y as VECTOR of Linear_Space_of_RealSequences by ;
set L1 = Linear_Space_of_RealSequences ;
set W = the_set_of_RealSequences_l^ p;
dom the addF of Linear_Space_of_RealSequences = by FUNCT_2:def 1;
then A6: dom () = by RELAT_1:62;
the_set_of_RealSequences_l^ p is linearly-closed by ;
then x + y = () . [x,y] by
.= x1 + y1 by ;
hence x + y = () + () by RSSPACE:2; :: thesis: verum
end;
A7: for r being Real
for x being VECTOR of lp holds r * x = r (#) ()
proof
set W = the_set_of_RealSequences_l^ p;
set L1 = Linear_Space_of_RealSequences ;
let r be Real; :: thesis: for x being VECTOR of lp holds r * x = r (#) ()
reconsider r = r as Element of REAL by XREAL_0:def 1;
let x be VECTOR of lp; :: thesis: r * x = r (#) ()
dom the Mult of Linear_Space_of_RealSequences = by FUNCT_2:def 1;
then A8: dom = by ;
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:10;
the_set_of_RealSequences_l^ p is linearly-closed by ;
then r * x = . [r,x] by
.= r * x1 by ;
hence r * x = r (#) () by RSSPACE:3; :: thesis: verum
end;
the_set_of_RealSequences_l^ p is linearly-closed by ;
then A9: 0. lp = 0. Linear_Space_of_RealSequences by
.= Zeroseq ;
A10: for x being set holds
( x is Element of lp iff ( x is Real_Sequence & () rto_power p is summable ) )
proof
let x be set ; :: thesis: ( x is Element of lp iff ( x is Real_Sequence & () rto_power p is summable ) )
( x in the_set_of_RealSequences_l^ p iff ( () rto_power p is summable & x in the_set_of_RealSequences ) ) by ;
hence ( x is Element of lp iff ( x is Real_Sequence & () rto_power p is summable ) ) by ; :: thesis: verum
end;
A11: 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 ;
hence ( x is VECTOR of lp implies x = seq_id x ) by A1, A2, Def2; :: thesis: verum
end;
A12: for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () )
proof
let x be VECTOR of lp; :: thesis: ( - x = - () & seq_id (- x) = - () )
lp is Subspace of Linear_Space_of_RealSequences by A1, A2, Th9;
then - x = (- 1) * x by RLVECT_1:16
.= - () by A7 ;
hence ( - x = - () & seq_id (- x) = - () ) ; :: thesis: verum
end;
for x, y being VECTOR of lp holds x - y = () - ()
proof
let x, y be VECTOR of lp; :: thesis: x - y = () - ()
thus x - y = () + (seq_id (- y)) by A4
.= () - () by A12 ; :: 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 & () 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 = () + () ) & ( for r being Real
for x being VECTOR of lp holds r * x = r (#) () ) & ( for x being VECTOR of lp holds
( - x = - () & seq_id (- x) = - () ) ) & ( for x, y being VECTOR of lp holds x - y = () - () ) & ( for x being VECTOR of lp holds () rto_power p is summable ) & ( for x being VECTOR of lp holds = (Sum (() rto_power p)) to_power (1 / p) ) ) by A2, A10, A11, A9, A4, A7, A12, A3; :: thesis: verum